syntax matches when literal doesn't

Stream: mathlib4

[Floris van Doorn]

I'm trying to refactor the way the to_additive syntax is parsed, but while doing that I stumbled upon interesting weird behavior, potentially a bug. I minimized it in the following code. It seems that the pattern (attr| to_additive (attrs := $[$stxs],*) seems to match the syntax to_additive (reorder := 1 2 3). Is this expected behavior?

import Mathlib.Tactic.RunCmd

open Lean Elab Command

syntax toAdditiveOption :=
  "(" (&"attrs" ":=" Parser.Term.attrInstance,*) <|> (&"reorder" ":=" num+ ) ")"

syntax (name := to_additive) "to_additive" toAdditiveOption : attr

def elabToAdditive : Syntax → CoreM Unit
  -- this pattern seems to match both cases
  | `(attr| to_additive (attrs := $[$stxs],*)) =>
    logInfo m!"attrs {stxs}"
  | `(attr| to_additive (reorder := $[$reorders:num]*)) =>
    logInfo m!"reorder {reorders.map (·.raw.isNatLit?.get!)}"
  | _ => throwUnsupportedSyntax

-- the same function, but with the patterns in different order. This works as expected (probably because `simp` is not a list of numerals)
def elabToAdditive2 : Syntax → CoreM Unit
  | `(attr| to_additive (reorder := $[$reorders:num]*)) =>
    logInfo m!"reorder {reorders.map (·.raw.isNatLit?.get!)}"
  | `(attr| to_additive (attrs := $[$stxs],*)) =>
    logInfo m!"attrs {stxs}"
  | _ => throwUnsupportedSyntax

run_cmd liftCoreM <| do
  elabToAdditive (← `(attr| to_additive (reorder := 1 2 3))) -- attrs [1, 3] (expected: reorder [1, 2, 3])
  elabToAdditive2 (← `(attr| to_additive (reorder := 1 2 3))) -- reorder [1, 2, 3] (as expected)
  elabToAdditive (← `(attr| to_additive (attrs := simp))) -- attrs [simp] (as expected)
  elabToAdditive2 (← `(attr| to_additive (attrs := simp))) -- attrs [simp] (as expected)

[Floris van Doorn]

The PR where I use this is mathlib4#1780

[Sebastian Ullrich]

(...) is not well-behaved with <|>. You should move the two sides to separate syntax := abbrevs.

[Floris van Doorn]

Ah, good to know. I can confirm that replacing the syntax with

syntax toAdditiveAttrsOption := &"attrs" ":=" Parser.Term.attrInstance,*
syntax toAdditiveReorderOption := &"reorder" ":=" num+
syntax toAdditiveOption := "(" toAdditiveAttrsOption <|> toAdditiveReorderOption ")"

gives the expected behavior.