From 43fc18eb41a9b6aa730eaf06fb073d67aa517f0e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Dec 2019 13:31:24 -0800
Subject: [PATCH] fix: incorrect local context being used to create new
 metavariables

---
 src/Init/Lean/Meta/Basic.lean         | 11 ++++++++---
 src/Init/Lean/Meta/SynthInstance.lean | 19 ++++++++++++-------
 tests/lean/run/meta2.lean             | 10 ++++++++++
 3 files changed, 30 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 25a93fe0ae..a816488977 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -203,12 +203,17 @@ do s ← get;
    modify $ fun s => { ngen := s.ngen.next, .. s };
    pure id
 
+def mkFreshExprMVarAt
+    (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false)
+    : MetaM Expr :=
+do mvarId ← mkFreshId;
+   modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type synthetic, .. s };
+   pure $ mkMVar mvarId
+
 def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false) : MetaM Expr :=
 do lctx ← getLCtx;
    localInsts ← getLocalInstances;
-   mvarId ← mkFreshId;
-   modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type synthetic, .. s };
-   pure $ mkMVar mvarId
+   mkFreshExprMVarAt lctx localInsts type userName synthetic
 
 def mkFreshLevelMVar : MetaM Level :=
 do mvarId ← mkFreshId;
diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 2205eb5e6d..550df53783 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -208,12 +208,15 @@ withMCtx mctx $ do
   mvarType ← instantiateMVars mvarType;
   pure $ mkTableKey mctx mvarType
 
-private partial def mkInstanceTelescopeAux
-    (xs : Array Expr) : Array Expr → Nat → List Expr → Expr → Expr → MetaM (List Expr × Expr × Expr)
+/- Remark: `(lctx, localInsts)` is the local context before we created the telescope containing `xs`.
+   We must use `(lctx, localInsts)` to create the new fresh metavariables `mvar`, otherwise the
+   application `mvar xs` is not a higher order pattern. -/
+private partial def mkInstanceTelescopeAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr)
+    : Array Expr → Nat → List Expr → Expr → Expr → MetaM (List Expr × Expr × Expr)
 | subst, j, subgoals, instVal, Expr.forallE n d b c => do
   let d     := d.instantiateRevRange j subst.size subst;
   type ← mkForall xs d;
-  mvar ← mkFreshExprMVar type;
+  mvar ← mkFreshExprMVarAt lctx localInsts type;
   let arg := mkAppN mvar xs;
   let instVal := mkApp instVal arg;
   let subgoals := if c.binderInfo.isInstImplicit then mvar::subgoals else subgoals;
@@ -227,14 +230,16 @@ private partial def mkInstanceTelescopeAux
   else
     pure (subgoals, instVal, type)
 
-def mkInstanceTelescope (xs : Array Expr) (inst : Expr) : MetaM (List Expr × Expr × Expr) :=
+def mkInstanceTelescope (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Expr) : MetaM (List Expr × Expr × Expr) :=
 do instType ← inferType inst;
-   mkInstanceTelescopeAux xs #[] 0 [] inst instType
+   mkInstanceTelescopeAux lctx localInsts xs #[] 0 [] inst instType
 
 def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) :=
-do mvarType ← inferType mvar;
+do mvarType   ← inferType mvar;
+   lctx       ← getLCtx;
+   localInsts ← getLocalInstances;
    forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do
-     (subgoals, instVal, instTypeBody) ← mkInstanceTelescope xs inst;
+     (subgoals, instVal, instTypeBody) ← mkInstanceTelescope lctx localInsts xs inst;
      Meta.trace `Meta.synthInstance.tryResolve $ fun _ => mvarTypeBody ++ " =?= " ++ instTypeBody;
      condM (isDefEq mvarTypeBody instTypeBody)
        (do instVal ← mkLambda xs instVal;
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 18ee40e4d9..dfd5394480 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -399,6 +399,16 @@ do print "----- tst17 -----";
 
 #eval run [`Init.Control.State] tst17
 
+def tst18 : MetaM Unit :=
+do print "----- tst18 -----";
+   decEqNat ← mkDecEq nat;
+   (some r) ← synthInstance decEqNat | throw $ Exception.other "failed `DecidableEq Nat`";
+   print r;
+   pure ()
+
+#eval run [`Init.Control.State] tst18
+
+
 #exit
 
 def tst15 : MetaM Unit :=