fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom (#2502)

* fix: `withCollectingNewGoalsFrom`
do not collect old goals

* fix: update occurs check

* test: fix test `run/492.lean`

* docs: add docstring to `elabTermWithHoles`

* test: `refineFiltersOldMVars`

* test: fix `expected.out` name

* test: fix `expected.out` filename and line numbers

* docs: use long ascii dash instead of em dash

Co-authored-by: Scott Morrison <scott@tqft.net>

* docs: fix long line, mention lean4#2502

* docs: a couple more long lines

* test: fix line numbers

---------

Co-authored-by: Scott Morrison <scott@tqft.net>

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -124,24 +124,39 @@ where
     let newMVarIds ← getMVarsNoDelayed val
     /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
     let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
-    let newMVarIds ← if allowNaturalHoles then
-      pure newMVarIds.toList
-    else
+    /- Filter out all mvars that were created prior to `k`. -/
+    let newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved
+    /- If `allowNaturalHoles := false`, all natural mvarIds must be assigned.
+    Passing this guard ensures that `newMVarIds` does not contain unassigned natural mvars. -/
+    unless allowNaturalHoles do
       let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
-      let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural
-      let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
       logUnassignedAndAbort naturalMVarIds
-      pure syntheticMVarIds.toList
     /-
     We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created.
     See issue #1682.
     Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they
     appear in the `.lean` file. We should tell users to prefer tagged goals.
     -/
-    let newMVarIds ← sortMVarIdsByIndex newMVarIds
+    let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList
     tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
     return (val, newMVarIds)
 
+/-- Elaborates `stx` and collects the `MVarId`s of any holes that were created during elaboration.
+
+With `allowNaturalHoles := false` (the default), any new natural holes (`_`) which cannot
+be synthesized during elaboration cause `elabTermWithHoles` to fail. (Natural goals appearing in
+`stx` which were created prior to elaboration are permitted.)
+
+Unnamed `MVarId`s are renamed to share the main goal's tag. If multiple unnamed goals are
+encountered, `tagSuffix` is appended to the main goal's tag along with a numerical index.
+
+Note:
+* Previously-created `MVarId`s which appear in `stx` are not returned.
+* All parts of `elabTermWithHoles` operate at the current `MCtxDepth`, and therefore may assign
+metavariables.
+* When `allowNaturalHoles := true`, `stx` is elaborated under `withAssignableSyntheticOpaque`,
+meaning that `.syntheticOpaque` metavariables might be assigned during elaboration. This is a
+consequence of the implementation. -/
 def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
   withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles
 
@@ -154,11 +169,18 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
     let (val, mvarIds') ← elabTermWithHoles stx (← getMainTarget) tagSuffix allowNaturalHoles
     let mvarId ← getMainGoal
     let val ← instantiateMVars val
-    unless val == mkMVar mvarId do
+    if val == mkMVar mvarId then
+      /- `val == mkMVar mvarId` is `true` when we've refined the main goal. Refining the main goal
+      (e.g. `refine ?a` when `?a` is the main goal) is an unlikely practice; further, it shouldn't
+      be possible to create new mvarIds during elaboration when doing so. But in the rare event
+      that somehow this happens, this is how we ought to handle it. -/
+      replaceMainGoal (mvarId :: mvarIds')
+    else
+      /- Ensure that the main goal does not occur in `val`. -/
       if val.findMVar? (· == mvarId) matches some _ then
         throwError "'refine' tactic failed, value{indentExpr val}\ndepends on the main goal metavariable '{mkMVar mvarId}'"
       mvarId.assign val
-    replaceMainGoal mvarIds'
+      replaceMainGoal mvarIds'
 
 @[builtin_tactic «refine»] def evalRefine : Tactic := fun stx =>
   match stx with

tests/lean/refineFiltersOldMVars.lean

@@ -0,0 +1,109 @@
+import Lean
+
+/-! These tests ensure that `refine e` only returns goals that were created during elaboration of
+`e` (and not before).
+
+Including mvars encountered in `e` that were created at any point in time caused trouble in a
+couple of ways:
+
+* Pre-existing goals were duplicated in the infoview (issue #2495)
+* "Goal tunneling": natural holes (`_`) created far earlier in the term could suddenly resurface
+  after using `refine` on a term that happened to involve them (not documented on the lean4 repo;
+  discovered during testing in Mathlib). A schematic example of this sort of issue:
+```
+def x := {
+  /- `field1` introduces a natural mvar: -/
+  field1 := f _
+  /- the value of `field1` is used in `field2`, and prior to this fix, the goal created above
+  "tunnels" into the infoview via `refine'`: -/
+  field2 := by refine' <term involving field1> -- includes pre-existing natural mvar
+}
+```
+
+These issues were fixed in lean4#2502.
+-/
+
+/-! # Issue 2495 -/
+
+/- In the following tests we take advantage of the fact that the unsolved goals error reports the
+tactic state to ensure that goals haven't been duplicated. -/
+
+/-! Refining using an existing goal (in this case, simply unifying it with the main goal) should
+only produce one `case a` in the infoview, not two. -/
+
+example : True := by
+  have : True := ?a
+  refine ?a -- should produce only one `case a`
+
+/-! Only new goals in the refined expression should replace the main goal. Pre-existing side goals
+should stay at the bottom of the list. -/
+
+inductive Foo where
+| mk (α : Type) : α → Foo
+
+example : Foo := by
+  have h : Type := ?a
+  refine .mk ?a ?b
+  /- `?a` is a pre-existing goal, `?b` is not; `refine` should only return `?b`, and `?a` should
+  remain at the bottom of the goal list. -/
+
+/-! # Goal tunneling -/
+
+/-! Natural mvars created earlier should not be able to tunnel into later uses of `refine`, but
+should be solved separately. -/
+
+axiom neq3 {n} : n ≠ 3
+
+structure Bar where
+  x : Nat
+  y : x ≠ 3
+
+/- This should not work: -/
+def bar : Bar := {
+  x := _ + 1
+  y := by
+    refine' neq3 -- captures the underscore above
+    exact 0 -- solves it
+}
+
+/-!
+# Issue #2434
+
+Resolving this issue also resolves issue #2434, which identified an inconsistency in *which*
+pre-existing mvars were being preserved --- namely, `refine` would include old pre-existing
+syntheticOpaque mvars, but not old natural mvars. This would erroneously close goals. Here, we
+demonstrate that uniformly filtering out old mvars also resolves that issue.
+-/
+
+open Lean Meta Elab Tactic Term in
+/-- `add_natural_goal a : A` adds a new natural goal of type `A` named `a` to the end of the tactic
+state. -/
+elab "add_natural_goal" s:ident " : " t:term : tactic => do
+  let g ← mkFreshExprMVar (← elabType t) .natural s.getId
+  appendGoals [g.mvarId!]
+
+/-!
+In the following, prior to lean4#2502, `refine` would erroneously close each focused goal, leading
+to a `(kernel) declaration has metavariables '_example'` error.
+This occurred because `withCollectingNewGoalsFrom` was only erroring on new natural goals (as
+determined by `index`), while simultaneously only passing through non-natural goals to construct
+the resulting goal list. This orphaned old natural metavariables and closed the goal list
+erroneously.
+As such, since we now eliminate all old mvars from the resulting goal list with the exception of
+the main goal (in which case we effectively no-op) all of the following tests should produce an
+`unsolved goals` error.
+-/
+
+example : Bool × Nat := by
+  add_natural_goal d : Bool
+  add_natural_goal e : Nat
+  · refine (?d,?e)
+  · refine ?d
+  · refine ?e
+
+example : Bool × Bool := by
+  add_natural_goal d : Bool
+  add_natural_goal e : Bool
+  · refine (?d,?e)
+  · case d => refine ?e
+  · refine ?e

tests/lean/refineFiltersOldMVars.lean.expected.out

@@ -0,0 +1,20 @@
+refineFiltersOldMVars.lean:34:18-36:11: error: unsolved goals
+case a
+⊢ True
+refineFiltersOldMVars.lean:44:17-46:18: error: unsolved goals
+case b
+h : Type
+⊢ ?a
+
+case a
+⊢ Type
+refineFiltersOldMVars.lean:66:4-66:11: error: no goals to be solved
+refineFiltersOldMVars.lean:101:2-101:3: error: unsolved goals
+case d
+⊢ Bool
+refineFiltersOldMVars.lean:102:2-102:3: error: unsolved goals
+case e
+⊢ Nat
+refineFiltersOldMVars.lean:109:2-109:3: error: unsolved goals
+case e
+⊢ Bool

tests/lean/run/492.lean

@@ -15,4 +15,4 @@ example : ∃ n : Nat, n = n := by
   refine ⟨?n, ?h⟩
   case h =>
     refine rfl
-    case n => exact 3
+  case n => exact 3