Syntax match not forcing types

Stream: lean4

[Reinier van der Gronden]

In the following MWE, I want to match on the syntax of an introduction tactic - but only the one where the input is a list of identifiers, not where fancy patterns are used. The example at the bottom shows that when using this tactic with something that in my opinion should not match, it still does. The variable ids is typed as TSyntaxArray 'ident, but it is clearly not when looking at the raw representation. Why is this? How else can you match on specific implementations of the intro tactic?

Tag for @Jannis Limperg , who was also curious about this.

import Lean
open
  Lean
  Lean.Elab.Tactic
#eval Lean.versionString -- 4.0.0-nightly-2022-11-09

def myTactic (t : TSyntax `tactic) : TacticM Unit := do
  match t with
  | `(tactic|intro $ids:ident*) =>
    -- ids is supposed to be TSyntaxArray `ident, but its content is not:
    addTrace `test m!"{ids.map (fun id => repr id.raw)}"
    --[Lean.Syntax.node
    --  (Lean.SourceInfo.none)
    --  `Lean.Parser.Term.anonymousCtor
    -- ...
    -- ]
  | _ => pure ()


elab &"myTactic " t:tactic : tactic =>
  myTactic t

example : α ∧ β → α := by
  myTactic intro ⟨ha, _⟩
  sorry

[Mario Carneiro]

I'm somewhat surprised intro $ids:ident* works / is not a type error. intro $[$ids:ident]* has the intended behavior, and should be required for this kind of pattern matching

[Reinier van der Gronden]

That's interesting, then what is the difference between those notations? In the builtintactic intro, they do a match with :term*, so I thought that was the general way to catch a list of syntax category objects.

[Mario Carneiro]

The $t* or $t:term* is an atomic binder, it just matches the entire syntax array argument without any further processing. The $[...]* syntax says to go into each element of the array and do a further match to bind things and pattern match the innards further (which is more expensive). It's roughly analogous to a pattern like | (t : List Term) => vs | [(t : Ident)] =>, the first one does no further matches and just binds what remains as t of type List Term while the second one does a match to check that the list has a specific form and binds an inner element.