From 34332ecaa9f9cf839c4cc9e04e4f659569a34b62 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Dec 2019 18:08:41 -0800
Subject: [PATCH] fix: `forallBoundedTelescope`

---
 src/Init/Lean/Meta/Basic.lean | 21 ++++++++++++---------
 tests/lean/run/meta4.lean     |  4 ++++
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index e8adebe1c3..5af0b083fb 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/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
diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean
index 8eb1120d72..9219811936 100644
--- a/tests/lean/run/meta4.lean
+++ b/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