Wrong type in hover on nested `sepBy` antiquotation

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The hover in a nested sepBy antiquotation displays the wrong type.

Context

Discovered while working on the auto-formatter and being very confused for how to write these nested anti-quotations after looking at the hover.

Steps to Reproduce

import Lean
open Lean                                                                     
                
-- Hover over `patss` in the pattern.                               
-- Expected: `Array (Syntax.TSepArray `term ",")`
-- Actual:   `Syntax.TSepArray `term ","`                                     
example (alt : TSyntax ``Parser.Term.matchAlt) : Option Nat := Id.run do      
  match alt with                                                              
  | `(Parser.Term.matchAltExpr| | $[$patss,*]|* => $_) =>                                                                 
    let _ : Array (Syntax.TSepArray `term ",") := patss                       
    return some 1                                                             
  | _ => return none
                                                                              
-- Enable to see both `patss` binders registered at the same source range:    
-- set_option trace.Elab.info true
-- example (alt : TSyntax ``Parser.Term.matchAlt) : Option Nat := Id.run do   
--   match alt with
--   | `(Parser.Term.matchAltExpr| | $[$patss,*]|* => $_) => return some 1    
--   | _ => return none

Versions

4.30.0-rc2

Additional Information

Pre-investigation by Claude:

The $[$patss,*]|* pattern expands to two
bindings both named patss at the same source range.

From the InfoTree trace:

• [Term] patss (isBinder := true) : Syntax.TSepArray
`term ","     @ ⟨7, 42⟩-⟨7, 47⟩
  ...
• [Term] patss (isBinder := true) : Array
(Syntax.TSepArray `term ",")  @ ⟨7, 42⟩-⟨7, 47⟩

The macro expansion (also visible in the trace) is:

match Array.mapM (fun x =>
    have __discr := x
    have patss := { elemsAndSeps := __discr.getArgs }  --
  inner: TSepArray `term ","
    some patss)
  __discr.getArgs.getSepElems with
| some patss =>
-- outer: Array (TSepArray `term ",")
  ...

Both patss binders carry the user's original source range
because they're both emitted using the user's $patss
identifier syntax (with its original SourceInfo). The
hover query lands in the inner lambda, so it picks the
inner TSepArray binder — that's what you were seeing.

The code that does it is in src/Lean/Elab/Quotation.lean:

- The inner binder is generated at line 397 (have $id :=
@TSepArray.mk ...) when quoteSyntax processes the nested
$patss,* splice inside the outer $[...]|*.
- The outer binder is the some $resId pattern at line
440, where resId = id for the single-id case (lines
426–427).

Both reuse $id → user's identifier → same position. A fix
would be to strip the source info on the inner $id (it's
an internal implementation detail, not the user-visible
binder) so only the outer binder carries the user's
range.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the hover mismatch with the nested sepBy antiquotation in a minimal test case. Read src/Lean/Elab/Quotation.lean around lines 397, 426–427, and 440, then inspect the generated binders and source ranges; done means hovering over patss reports Array (Syntax.TSepArray `term ",") rather than the inner type.