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
+  let mut alreadyVisited : MVarIdSet := {}
-    |>.map (·.mvarId)
+  let mut result : MVarIdSet := {}
-    |>.filterM λ mvarId =>
+  for mvarErrorInfo in (← get).mvarErrorInfos do
-      return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
+    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 ·)