Constrained Enumerators trigger stack overflow when too much fuel is provided

[ngernest]

When a fuel parameter of more than 3 is supplied to a constrained numerator derived from an inductive relation (i.e. an instance of the EnumSizedSuchThat typeclass), we encounter a stack overflow issue.

See Test/DeriveEnumSuchThat/DerivePermutationEnumerator.lean for an example. To run the enumerator, you can do the following:

def l' := [1, 2, 3]

--  This prints out `[some [2, 1, 3], some [1, 3, 2], ...]`
-- However, changing `size` to 3 causes stack overflow
#eval runSizedEnum (EnumSizedSuchThat.enumSizedST (fun l => Permutation l l') (size := 2)

Right now, the implementation of lazy lists (see LazyList.lean), which underpin enumerators, follows the QuickChick source code very closely, although I am not entirely sure what is the origin of this bug. I wonder if switching to a (thunked) representation based on Haskell's difference lists will address this issue, since enumerators use LazyLists under append-heavy workloads, and difference lists support amortized O(1) append operations.

As a temporary workaround, when a derived checker invokes a constrained enumerator (e.g. for existentially quantified variables), we pass in (min 2 initSize) as the fuel for the enumerator in the derived checker code -- see this PR for details.

[ngernest]

Note that this issue remains even if we convert each sub-enumerator to a thunk. Consider this example in Examples/Trees.lean (see the thunkify_enumerators branch for the full code + versions of enumerator combinators which work over thunked sub-enumerators):

/-- A hand-written enumerator for balanced trees, where all sub-generators are thunked -/
def enumBalancedTree (n_1 : Nat) : Nat → OptionT Enumerator Tree :=
  let rec aux_enum (initSize : Nat) (size : Nat) (n_1 : Nat) : OptionT Enumerator Tree :=
      match size with
      | Nat.zero =>
        EnumeratorCombinators.enumerateThunk
          [mkThunk $ match n_1 with
            | Nat.zero => return Tree.Leaf
            | _ => OptionT.fail,
            mkThunk $ match n_1 with
            | Nat.succ (Nat.zero) => return Tree.Leaf
            | _ => OptionT.fail]
      | Nat.succ size' =>
        EnumeratorCombinators.enumerateThunk
          [mkThunk $ match n_1 with
            | Nat.zero => return Tree.Leaf
            | _ => OptionT.fail,
            mkThunk $ match n_1 with
            | Nat.succ (Nat.zero) => return Tree.Leaf
            | _ => OptionT.fail,
            mkThunk $ match n_1 with
            | Nat.succ n => do
              let l ← aux_enum initSize size' n;
              do
                let r ← aux_enum initSize size' n;
                do
                  let x ← Enum.enum;
                  return Tree.Node x l r
            | _ => OptionT.fail]
    fun size => aux_enum size size n_1

-- Changing size to `3` or any larger `Nat` causes stack overflow
-- def size := 2
-- #eval runSizedEnum (enumBalancedTree 2) size