conflicting asterisk for syntax matching

Stream: lean4

[Arthur Paulino]

The asterisk * to symbolize Array Syntax seems to be conflicting with the one from a previously defined syntax. #mwe:

declare_syntax_cat foo
syntax foo " * " foo : foo -- comment this line
syntax ident foo* : foo

macro_rules
  | `(foo| $x:foo * $y:foo) => sorry -- comment this line too and it will work
  | `(foo| $id:ident $ys:foo*) => sorry -- expected foo

If you comment out those indicated lines the code works. Has anyone seen this before?

[Sebastian Ullrich]

I'm not terribly sure what's going on, but

  | `(foo| $id:ident $[$ys:foo]*) => sorry -- expected foo

works

[Arthur Paulino]

But then ys is no longer of Array Syntax, but rather of Syntax

[Sebastian Ullrich]

Don't trust the type hover

[Sebastian Ullrich]

Sebastian Ullrich said:

I'm not terribly sure what's going on

Ah. $ys:foo* is not actually a single notation. The parser foo* will try to parse a single foo, then check if it was an antiquotation and whether there is a trailing *. But parsing that single foo will already consume the * because of the first syntax declaration, and error out.

[Arthur Paulino]

Sebastian Ullrich said:

Don't trust the type hover

But I can't even call getElems

| `(expression| $x:ident $[$ys:expression]*) => do
    let qq := ys.getElems
    -- invalid field 'getElems', the environment does not contain 'Array.getElems'
    --   ys
    -- has type
    --   Array Syntax

[Arthur Paulino]

Wait, it's already of type Array Syntax :thinking: