From 0c469027c6ccb84f14c2c097dbc96c2e152cdbc6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 17 Aug 2024 00:50:02 -0700
Subject: [PATCH] fix: Refactor mvar collection in assign tactic

---
 Pantograph/Tactic/Assign.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
index ea08c48..acf5d16 100644
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@@ -4,7 +4,8 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
+/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
+def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
   goal.checkNotAssigned `Pantograph.Tactic.assign
 
   -- This run of the unifier is critical in resolving mvars in passing
@@ -12,19 +13,18 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
   let goalType ← goal.getType
   unless ← Meta.isDefEq goalType exprType do
     throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
-
-  -- FIXME: Use `withCollectingNewGoalsFrom`. Think about how this interacts with elaboration ...
-  let nextGoals ← Meta.getMVarsNoDelayed expr
   goal.assign expr
-  nextGoals.toList.filterM (not <$> ·.isAssigned)
+  nextGoals.filterM (not <$> ·.isAssigned)
 
 def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   let target ← Elab.Tactic.getMainTarget
+  let goal ← Elab.Tactic.getMainGoal
+  goal.checkNotAssigned `Pantograph.Tactic.evalAssign
   let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
     (expectedType? := .some target)
     (tagSuffix := .anonymous )
     (allowNaturalHoles := true)
-  (← Elab.Tactic.getMainGoal).assign expr
+  goal.assign expr
   Elab.Tactic.setGoals nextGoals