fix: use mkForallFVars and mkLambdaFVars

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 }
 

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
 

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 := [])