From e79370a1e61a346c192b839cec1f9cc6542f4e3e Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Thu, 21 Sep 2023 00:23:27 -0400 Subject: [PATCH] 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 * docs: fix long line, mention lean4#2502 * docs: a couple more long lines * test: fix line numbers --------- Co-authored-by: Scott Morrison --- src/Lean/Elab/Tactic/ElabTerm.lean | 40 +++++-- tests/lean/refineFiltersOldMVars.lean | 109 ++++++++++++++++++ .../refineFiltersOldMVars.lean.expected.out | 20 ++++ tests/lean/run/492.lean | 2 +- 4 files changed, 161 insertions(+), 10 deletions(-) create mode 100644 tests/lean/refineFiltersOldMVars.lean create mode 100644 tests/lean/refineFiltersOldMVars.lean.expected.out diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index dce00625b0..4e51e416f6 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/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 diff --git a/tests/lean/refineFiltersOldMVars.lean b/tests/lean/refineFiltersOldMVars.lean new file mode 100644 index 0000000000..3c3348cb59 --- /dev/null +++ b/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' -- 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 diff --git a/tests/lean/refineFiltersOldMVars.lean.expected.out b/tests/lean/refineFiltersOldMVars.lean.expected.out new file mode 100644 index 0000000000..f0912d5d24 --- /dev/null +++ b/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 diff --git a/tests/lean/run/492.lean b/tests/lean/run/492.lean index 8ea1197237..289ad8a68a 100644 --- a/tests/lean/run/492.lean +++ b/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