fix: forallBoundedTelescope

src/Init/Lean/Meta/Basic.lean

@@ -508,19 +508,22 @@ resettingSynthInstanceCache $
     (reducing?        : Bool) (maxFVars? : Option Nat)
     (k                : Array Expr → Expr → MetaM α)
     : LocalContext → Array Expr → Nat → Expr → MetaM α
-| lctx, fvars, j, Expr.forallE n d b c => do
-  let d     := d.instantiateRevRange j fvars.size fvars;
-  fvarId ← mkFreshId;
-  let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo;
-  let fvar  := mkFVar fvarId;
-  let fvars := fvars.push fvar;
+| lctx, fvars, j, type@(Expr.forallE n d b c) => do
+  let process : Unit → MetaM α := fun _ => do {
+    let d     := d.instantiateRevRange j fvars.size fvars;
+    fvarId ← mkFreshId;
+    let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo;
+    let fvar  := mkFVar fvarId;
+    let fvars := fvars.push fvar;
+    forallTelescopeReducingAuxAux lctx fvars j b
+  };
   match maxFVars? with
-  | none          => forallTelescopeReducingAuxAux lctx fvars j b
+  | none          => process ()
   | some maxFVars =>
     if fvars.size < maxFVars then
-      forallTelescopeReducingAuxAux lctx fvars j b
+      process ()
     else
-      let type := b.instantiateRevRange j fvars.size fvars;
+      let type := type.instantiateRevRange j fvars.size fvars;
       adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
         withNewLocalInstances isClassExpensive fvars j $
           k fvars type

tests/lean/run/meta4.lean

@@ -32,6 +32,10 @@ print e;
 (_, _, e') ← forallMetaTelescopeReducing cinfo.type;
 print e';
 check (isDefEq e e');
+forallBoundedTelescope cinfo.type (some 0) $ fun xs body => check (pure (xs.size == 0));
+forallBoundedTelescope cinfo.type (some 1) $ fun xs body => check (pure (xs.size == 1));
+forallBoundedTelescope cinfo.type (some 6) $ fun xs body => do { print xs; check (pure (xs.size == 6)) };
+forallBoundedTelescope cinfo.type (some 10) $ fun xs body => do { print xs; check (pure (xs.size == 6)) };
 pure ()
 
 #eval tst1