Syntax matching and overloaded syntax

Stream: lean4

[Eric Wieser]

Is this expected behavior?

import Lean

open Lean Meta Elab

syntax (name := fooCmd) group("foo " declId ) : command

def isFoo (stx : Syntax.Command) : Bool := stx matches `(command| foo $name:declId)

-- works as expected: true
#eval show MetaM _ from return isFoo ⟨← `(command| foo bar)⟩

syntax (name := foo2Cmd) group("foo " declId ) : command

-- fails: false!
#eval show MetaM _ from return isFoo ⟨← `(command| foo bar)⟩

def isFoo' (stx : Syntax.Command) : Bool := stx matches `(command| foo $name:declId)

-- works as expected: true
#eval show MetaM _ from return isFoo' ⟨← `(command| foo bar)⟩

[Eric Wieser]

That is, the introduction of overloaded syntax causes choice nodes to be inserted in subsequent syntax, but the original matcher doesn't look for this node

[Eric Wieser]

(the context here is that both mathlib and batteries define identical lemma syntax)