incorrect hover type for array in syntax quote destruct

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

import Lean

open Lean Elab Tactic

syntax (name := just_print) "just_print" (ppSpace colGt term)* : tactic

@[tactic just_print]
def justPrintImpl : Tactic
| `(tactic| just_print $[$xs]*) => do
  let xs : Array (TSyntax `term) := xs
  logInfo f!"{xs}"
  return
| _ => throwUnsupportedSyntax

Expected behavior:

hover xs : Array (TSyntax term)`

Actual behavior:

hover xs : TSyntax term`

Versions

4.10.0-rc2

macOS

Impact

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

Start with the minimal reproducer and the justPrintImpl syntax-quote destructuring shown in the issue. Trace how hover information is produced for the bound xs value, then reproduce the behavior on the reported Lean version or current nightly. Done means hovering xs reports Array (TSyntax term)rather thanTSyntax term.