From f01471f6203168c8ab349e552214d552bebd229a Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 8 Jan 2025 09:36:45 +0100 Subject: [PATCH] fix: proper "excess binders" error locations for `rintro` and `intro` (#6565) This PR fixes the location of the error emitted when the `rintro` and `intro` tactics cannot introduce the requested number of binders. This patch adds a few `withRef` wrappers to invocations of `MVarId.intro` to fix error locations. Perhaps `MVarId.intro` should take a syntax object to set the location itself in the future; however there are a couple other call sites which would need non-trivial fixup. Closes #5659. --- src/Init/Prelude.lean | 10 +++++++++ src/Lean/Elab/Tactic/BuiltinTactic.lean | 8 +++---- src/Lean/Elab/Tactic/RCases.lean | 2 +- tests/lean/interactive/5659.lean | 13 +++++++++++ tests/lean/interactive/5659.lean.expected.out | 22 +++++++++++++++++++ .../incrementalTactic.lean.expected.out | 5 +++-- 6 files changed, 53 insertions(+), 7 deletions(-) create mode 100644 tests/lean/interactive/5659.lean create mode 100644 tests/lean/interactive/5659.lean.expected.out diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 0d9514ae77..0253c5df6f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4170,6 +4170,16 @@ def withRef [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α := let ref := replaceRef ref oldRef MonadRef.withRef ref x +/-- +If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`. +Otherwise, run `x` directly. +-/ +@[always_inline, inline] +def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m α := + match ref? with + | some ref => withRef ref x + | _ => x + /-- A monad that supports syntax quotations. Syntax quotations (in term position) are monadic values that when executed retrieve the current "macro scope" from the monad and apply it to every identifier they introduce diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index aa02a0f849..72c5d139c4 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -362,9 +362,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*)) | _ => throwUnsupportedSyntax where - introStep (ref : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do + introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do let fvarId ← liftMetaTacticAux fun mvarId => do - let (fvarId, mvarId) ← mvarId.intro n + let (fvarId, mvarId) ← withRef? ref? <| mvarId.intro n pure (fvarId, [mvarId]) if let some typeStx := typeStx? then withMainContext do @@ -374,9 +374,9 @@ where unless (← isDefEqGuarded type fvarType) do throwError "type mismatch at `intro {fvar}`{← mkHasTypeButIsExpectedMsg fvarType type}" liftMetaTactic fun mvarId => return [← mvarId.replaceLocalDeclDefEq fvarId type] - if let some stx := ref then + if let some ref := ref? then withMainContext do - Term.addLocalVarInfo stx (mkFVar fvarId) + Term.addLocalVarInfo ref (mkFVar fvarId) @[builtin_tactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do let matchAlts := stx[1] diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean index d8ecac3b21..31d3ecac71 100644 --- a/src/Lean/Elab/Tactic/RCases.lean +++ b/src/Lean/Elab/Tactic/RCases.lean @@ -507,7 +507,7 @@ partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a match pat with | `(rintroPat| $pat:rcasesPat) => let pat := (← RCasesPatt.parse pat).typed? ref ty? - let (v, g) ← g.intro (pat.name?.getD `_) + let (v, g) ← withRef pat.ref <| g.intro (pat.name?.getD `_) rcasesCore g fs clears (.fvar v) a pat cont | `(rintroPat| ($(pats)* $[: $ty?']?)) => let ref := if pats.size == 1 then pat.raw else .missing diff --git a/tests/lean/interactive/5659.lean b/tests/lean/interactive/5659.lean new file mode 100644 index 0000000000..92b03237bf --- /dev/null +++ b/tests/lean/interactive/5659.lean @@ -0,0 +1,13 @@ +/-! + # `rintro` and `intro` error message should point to excess arg + + Below, the errors should point to `h` because there is no lambda it binds. + The error should not point to `hn`; it would be OKish to underline the whole line. -/ + +example : (∃ n : Nat, n < 0) → False := by + rintro ⟨n, hn⟩ h + --^ collectDiagnostics + +example : (∃ n : Nat, n < 0) → False := by + intro ⟨n, hn⟩ h + --^ collectDiagnostics diff --git a/tests/lean/interactive/5659.lean.expected.out b/tests/lean/interactive/5659.lean.expected.out new file mode 100644 index 0000000000..95178ac230 --- /dev/null +++ b/tests/lean/interactive/5659.lean.expected.out @@ -0,0 +1,22 @@ +{"version": 1, + "uri": "file:///5659.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 7, "character": 17}, "end": {"line": 7, "character": 18}}, + "message": + "tactic 'introN' failed, insufficient number of binders\ncase intro\nn : Nat\nhn : n < 0\n⊢ False", + "fullRange": + {"start": {"line": 7, "character": 17}, + "end": {"line": 7, "character": 18}}}, + {"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 11, "character": 16}, + "end": {"line": 11, "character": 17}}, + "message": + "tactic 'introN' failed, insufficient number of binders\nn : Nat\nhn : n < 0\n⊢ False", + "fullRange": + {"start": {"line": 11, "character": 16}, + "end": {"line": 11, "character": 17}}}]} diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out index 706ae32c68..b429e40063 100644 --- a/tests/lean/interactive/incrementalTactic.lean.expected.out +++ b/tests/lean/interactive/incrementalTactic.lean.expected.out @@ -12,11 +12,12 @@ t 2 [{"source": "Lean 4", "severity": 1, "range": - {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}}, + {"start": {"line": 4, "character": 12}, "end": {"line": 4, "character": 13}}, "message": "tactic 'introN' failed, insufficient number of binders\na n : Nat\n⊢ True", "fullRange": - {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}}}, + {"start": {"line": 4, "character": 12}, + "end": {"line": 4, "character": 13}}}, {"source": "Lean 4", "severity": 1, "range":