From 1d10cd2b205f8baf172384733793cd2a55a1f5d8 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 23:16:33 -0800
Subject: [PATCH] fix: Collect errored mvars by iterating errorInfo

---
 Pantograph/Goal.lean | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 51aed88..f2eb25a 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -177,12 +177,25 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 --- Tactic execution functions ---
 
+-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
   let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
-  (← getThe Elab.Term.State).mvarErrorInfos
-    |>.map (·.mvarId)
-    |>.filterM λ mvarId =>
-      return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
+  let mut alreadyVisited : MVarIdSet := {}
+  let mut result : MVarIdSet := {}
+  for mvarErrorInfo in (← get).mvarErrorInfos do
+    let mvarId := mvarErrorInfo.mvarId
+    unless alreadyVisited.contains mvarId do
+      alreadyVisited := alreadyVisited.insert mvarId
+      /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
+         delayed assigned to another metavariable that is unassigned. -/
+      let mvarDeps ← Meta.getMVars (mkMVar mvarId)
+      if mvarDeps.any descendants.contains then do
+        result := result.insert mvarId
+  return result.toList
+  --(← getThe Elab.Term.State).mvarErrorInfos
+  --  |>.map (·.mvarId)
+  --  |>.filterM λ mvarId =>
+  --    return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
 
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
   let li2' := li2.filter (¬ li1.contains ·)