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] 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