From 0faaa5ac54a332945ccb09edf21ddea883f05793 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Sep 2020 08:33:16 -0700
Subject: [PATCH] fix: use `mkForallFVars` and `mkLambdaFVars`

---
 src/Lean/Elab/LetRec.lean    | 22 ++++++++++++----------
 src/Lean/Elab/MutualDef.lean |  9 +++++----
 src/Lean/Elab/Term.lean      | 19 ++++++++++---------
 3 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 25570f03ed..2ee82e4a11 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -97,16 +97,18 @@ when e.hasSyntheticSorry $ throwAbort
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
 lctx ← getLCtx;
-let toLift      := views.mapIdx fun i view => {
-  ref           := view.ref,
-  fvarId        := (fvars.get! i).fvarId!,
-  attrs         := view.attrs,
-  shortDeclName := view.shortDeclName,
-  declName      := view.declName,
-  lctx          := lctx,
-  type          := view.type,
-  val           := values.get! i,
-  mvarId        := view.mvar.mvarId!
+localInsts ← getLocalInstances;
+let toLift := views.mapIdx fun i view => {
+  ref            := view.ref,
+  fvarId         := (fvars.get! i).fvarId!,
+  attrs          := view.attrs,
+  shortDeclName  := view.shortDeclName,
+  declName       := view.declName,
+  lctx           := lctx,
+  localInstances := localInsts,
+  type           := view.type,
+  val            := values.get! i,
+  mvarId         := view.mvar.mvarId!
   : LetRecToLift };
 modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 4444b04bc3..c567d2d5e3 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -317,10 +317,11 @@ ps.mapM fun (p : Array Expr × LetRecToLift) => do
       | some p => some (mkAppN (Lean.mkConst p.2.declName) p.1)
       | none => none
     | _ => none;
-  -- Apply closure
-  let type := lctx.mkForall xs type;
-  let val  := lctx.mkLambda xs val;
-  pure { toLift with type := type, val := val }
+  withLCtx lctx toLift.localInstances do
+    -- Apply closure
+    type ← mkForallFVars xs type;
+    val  ← mkLambdaFVars xs val;
+    pure { toLift with type := type, val := val }
 
 end LetRecClosure
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 17010cac1d..65e82a244b 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -69,15 +69,16 @@ structure MVarErrorContext :=
 (ctx?   : Option Expr := none)
 
 structure LetRecToLift :=
-(ref           : Syntax)
-(fvarId        : FVarId)
-(attrs         : Array Attribute)
-(shortDeclName : Name)
-(declName      : Name)
-(lctx          : LocalContext)
-(type          : Expr)
-(val           : Expr)
-(mvarId        : MVarId)
+(ref            : Syntax)
+(fvarId         : FVarId)
+(attrs          : Array Attribute)
+(shortDeclName  : Name)
+(declName       : Name)
+(lctx           : LocalContext)
+(localInstances : LocalInstances)
+(type           : Expr)
+(val            : Expr)
+(mvarId         : MVarId)
 
 structure State :=
 (syntheticMVars    : List SyntheticMVarDecl := [])