fix: make sure refine preserves pre-existing natural mvars (leanprover#2435)

* fix: `withCollectingNewGoals`
* don't exclude pre-existing natural mvars

* test: ensure pre-existing natural mvars are preserved

* docs: update comment and include issue number

* test: expected.out

* docs: add module docstrings to test
* also deleted superfluous `add_synthetic_goal`

* test: fix expected.out line numbers

* Update tests/lean/refinePreservesNaturalMVars.lean

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

* docs: clarify comment

---------

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

Author: thorimur

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -124,21 +124,23 @@ 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
+    /- The following `unless … do` block guards against unassigned natural mvarids created during
+    `k` in the case that `allowNaturalHoles := false`. If we pass this block without aborting, we
+    can be assured that `newMVarIds` does not contain unassigned natural mvars created during `k`.
+    Note that in all cases we must allow `newMVarIds` to contain unassigned natural mvars which
+    were created *before* `k`; this is the purpose of `mvarCounterSaved`, which lets us distinguish
+    mvars created before `k` from those created during and after. See issue #2434. -/
+    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)
 

tests/lean/refinePreservesNaturalMVars.lean

@@ -0,0 +1,53 @@
+import Lean
+
+/-! Ensures that `refine` does not remove pre-existing natural goals from the goal list. -/
+
+open Lean Meta Elab Tactic Term
+
+elab "add_natural_goal" s:ident " : " t:term : tactic => do
+  let g ← mkFreshExprMVar (← elabType t) .natural s.getId
+  appendGoals [g.mvarId!]
+
+/-!
+
+In the following, `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, all of the following tests should lead to an `unsolved goals` error, followed by a
+`no goals` error (instead of a successful focus).
+
+-/
+
+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
+
+/-!
+
+Previously, this would error, as `refine (?d, ?e)` erroneously closed the goal, leading to a
+`no goals` error. Instead, this should succeed.
+
+-/
+
+example : Bool × Bool := by
+  add_natural_goal d : Bool
+  add_natural_goal e : Bool
+  · refine (?d,?e)
+    refine ?d
+    refine ?e   -- This unifies `?d` and `?e`, so only one goal remains.
+    exact true

tests/lean/refinePreservesNaturalMVars.lean.expected.out

@@ -0,0 +1,14 @@
+refinePreservesNaturalMVars.lean:29:2-29:3: error: unsolved goals
+case d
+⊢ Bool
+
+case e
+⊢ Nat
+refinePreservesNaturalMVars.lean:30:2-30:3: error: no goals to be solved
+refinePreservesNaturalMVars.lean:36:2-36:3: error: unsolved goals
+case d
+⊢ Bool
+
+case e
+⊢ Bool
+refinePreservesNaturalMVars.lean:37:2-37:3: error: no goals to be solved