Revert "fix: make sure refine preserves pre-existing natural mvars (#2435)" (#2485)

This reverts commit 0b64c1e330.

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -124,23 +124,21 @@ 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)
-    /- 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 newMVarIds ← if allowNaturalHoles then
+      pure newMVarIds.toList
+    else
       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.toList
+    let newMVarIds ← sortMVarIdsByIndex newMVarIds
     tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
     return (val, newMVarIds)
 

tests/lean/refinePreservesNaturalMVars.lean

@@ -1,53 +0,0 @@
-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

@@ -1,14 +0,0 @@
-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