Why does the elaborator fail with conflicting syntax?

Stream: metaprogramming / tactics

[Syed Shaazib Tanvir]

I have the following code

inductive Test where
  | abc
  | xyz

example (t : Test) : True := by
  induction t with
  | abc => trivial
  | xyz => trivial

declare_syntax_cat test_cat
syntax "abc" : test_cat

example (t : Test) : True := by
  induction t with
  | abc => trivial
  | xyz => trivial

In the example on the top it matches abc as expected but in the bottom one I get

unexpected token 'abc'; expected '_' or identifier

because of the syntax declaration
However, according to The Lean Language Reference

When multiple syntax rules for a category can match the current input, the local longest-match rule is used to select one of them. Like notations and operators, if there is a tie for the longest match then the declared priorities are used to determine which parse result applies. If this still does not resolve the ambiguity, then all the results that tied are saved. The elaborator is expected to attempt all of them, succeeding when exactly one can be elaborated.

Which should be the case here since there's no elaboration defined for abc, yet it still fails?

[Edward van de Meent]

i believe the issue is that abc is no longer a valid identifier, since the syntax declaration makes it reserved

[Edward van de Meent]

you can fix this by adding a & before the string in the syntax declaration:
syntax &"abc" : test_cat

[Edward van de Meent]

another (possibly more durable) option is to make your syntax scoped to some namespace. This way, abc will only be reserved in the namespace where you declare the syntax. If in that namespace you still want to refer to the identifier instead of the syntax, you can use french quotes: «abc»

[Sebastian Ullrich]

Edward van de Meent said:

i believe the issue is that abc is no longer a valid identifier, since the syntax declaration makes it reserved

In addition, the quoted text would not apply here in any case as no category is being parsed at that point

[Edward van de Meent]

not the ident category?

[Edward van de Meent]

or is that not a category? i'm guessing it's not a category then.

[Edward van de Meent]

yup, syntax "fooo[]":ident indeed fails complaining that ident is not a parser category.

[Syed Shaazib Tanvir]

Edward van de Meent said:

another (possibly more durable) option is to make your syntax scoped to some namespace. This way, abc will only be reserved in the namespace where you declare the syntax. If in that namespace you still want to refer to the identifier instead of the syntax, you can use french quotes: «abc»

In my bigger program I had a DSL with a skip command and the corresponding AST with a skip type constructor. The DSL was only elaborated when it was in the form ⟪ skip ⟫ so I was confused on why I was getting the error but this makes sense.

Thanks a lot for the help.