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

@@ -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

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]

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

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

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}}}]}

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":