From 657a61f8befd5c3b4fcbc54a53a9414af427a2e3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 13 Jul 2025 22:45:29 -0700
Subject: [PATCH 1/3] test(frontend): Capturing local instances

---
 Test/Frontend.lean | 26 +++++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index fec2e01..0fe94ff 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -182,6 +182,25 @@ example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
     }
   ])
 
+def test_sorry_with_local_instance : TestT MetaM Unit := do
+  let sketch := "
+def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s
+example (α : Type) [Inhabited α] : α := sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  let result ← runTermElabMInMeta $ goalState.tryTactic .unfocus "exact test α"
+  checkTrue "success" $ result matches .success ..
+  match result with
+  | .success .. => return ()
+  | .failure messages =>
+    let messages ← messages.mapM (·.toString)
+    fail s!"Could not execute tactic {messages}"
+  | .parseError e =>
+    fail s!"Parse error: {e}"
+  | .invalidAction e =>
+    fail s!"Invalid action: {e}"
+
 def test_environment_capture: TestT MetaM Unit := do
   let sketch := "
 def mystery (n: Nat) := n + 1
@@ -257,9 +276,10 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
-    ("sorry_in_middle", test_sorry_in_middle),
-    ("sorry_in_induction", test_sorry_in_induction),
-    ("sorry_in_coupled", test_sorry_in_coupled),
+    ("sorry in middle", test_sorry_in_middle),
+    ("sorry in induction", test_sorry_in_induction),
+    ("sorry in coupled", test_sorry_in_coupled),
+    ("sorry with local instances", test_sorry_with_local_instance),
     ("environment_capture", test_environment_capture),
     ("capture_type_mismatch", test_capture_type_mismatch),
     --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),

From 01e18acdbdab69988b716cf0973e59e6dcfcbff2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 13 Jul 2025 22:56:52 -0700
Subject: [PATCH 2/3] fix(frontend): Local instances in sorry capture

---
 Pantograph/Frontend/MetaTranslate.lean | 4 +++-
 Test/Main.lean                         | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
index 3d2829b..1f6d45d 100644
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -111,7 +111,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
   let lctx ← MonadLCtx.getLCtx
   assert! lctx.isEmpty
   (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do
+    let localDecl ← Meta.withLCtx' lctx do
       translateLocalDecl srcLocalDecl
     pure $ lctx.addDecl localDecl
   ) lctx
@@ -148,7 +148,9 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
   }) do
     let type := termInfo.expectedType?.get!
     let lctx' ← translateLCtx
+    --let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
     let mvar ← Meta.withLCtx lctx' #[] do
+      Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
       let type' ← translateExpr type
       trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'
diff --git a/Test/Main.lean b/Test/Main.lean
index fa08920..ffe9cf1 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -1,4 +1,3 @@
-import LSpec
 import Test.Delate
 import Test.Environment
 import Test.Frontend
@@ -9,6 +8,8 @@ import Test.Proofs
 import Test.Serial
 import Test.Tactic
 
+import LSpec
+
 -- Test running infrastructure
 
 namespace Pantograph.Test

From 3bbbb14da65ed93b79dfd9913215d796b56bdd2b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 13 Jul 2025 22:58:20 -0700
Subject: [PATCH 3/3] chore: Remove dead code

---
 Pantograph/Frontend/MetaTranslate.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
index 1f6d45d..cd3f09b 100644
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -148,7 +148,6 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
   }) do
     let type := termInfo.expectedType?.get!
     let lctx' ← translateLCtx
-    --let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
     let mvar ← Meta.withLCtx lctx' #[] do
       Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
       let type' ← translateExpr type