Fix LocalContext and LocalInstance captured by sorries for the tactic mode

REPL/Main.lean

@@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-          let lctx ← ctx.runMetaM {} do
-              match ctx.mctx.findDecl? g with
-              | some decl => return decl.lctx
-              | none => throwError "unknown metavariable '{g}'"
-          let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
+          let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
@@ -197,7 +193,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             unless (← Meta.isDefEq pft expectedType) do
               return s!"Error: proof has type {pft} but root goal has type {expectedType}"
 
-            let pf ← abstractAllLambdaFVars pf
+            let pf ← abstractAllLambdaFVars pf >>= instantiateMVars
             let pft ← Meta.inferType pf >>= instantiateMVars
 
             if pf.hasExprMVar then

REPL/Snapshots.lean

@@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
+
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
-
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
 def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
-  ctx.runMetaM (lctx?.getD {}) do
-    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    let s ← getThe Core.State
-    let s := match env? with
-    | none => s
-    | some env => { s with env }
-    pure <|
-    { coreState := s
-      coreContext := ← readThe Core.Context
-      metaState := ← getThe Meta.State
-      metaContext := ← readThe Meta.Context
-      termState := {}
-      termContext := {}
-      tacticState := { goals }
-      tacticContext := { elaborator := .anonymous }
-      rootGoals := match rootGoals? with
-        | none => goals
-        | some gs => gs }
+  -- Get the local context from the goals if not provided.
+  let lctx ← match lctx? with
+  | none => match goals with
+    | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx
+    | [] => match rootGoals? with
+      | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx
+      | _ => pure {}
+  | some lctx => pure lctx
+
+  ctx.runMetaM lctx do
+    -- update local instances, which is necessary when `types` is non-empty
+    Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
+      let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+      let s ← getThe Core.State
+      let s := match env? with
+      | none => s
+      | some env => { s with env }
+      pure <|
+      { coreState := s
+        coreContext := ← readThe Core.Context
+        metaState := ← getThe Meta.State
+        metaContext := ← readThe Meta.Context
+        termState := {}
+        termContext := {}
+        tacticState := { goals }
+        tacticContext := { elaborator := .anonymous }
+        rootGoals := match rootGoals? with
+          | none => goals
+          | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/

test/local_instance_proof.expected.out

@@ -0,0 +1,62 @@
+{"env": 0}
+
+{"env": 1}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 42},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 47}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 45},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 3}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"env": 4}
+
+{"sorries":
+ [{"proofState": 4,
+   "pos": {"line": 1, "column": 17},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 22}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 5}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"sorries":
+ [{"proofState": 6,
+   "pos": {"line": 1, "column": 20},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 25}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 6}
+
+{"proofStatus": "Completed", "proofState": 7, "goals": []}
+

test/local_instance_proof.in

@@ -0,0 +1,21 @@
+{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 2}
+
+{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0}
+
+{"cmd": "def test2 : α := sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 4}
+
+{"cmd": "def test2 : α := by sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 6}