Syntax quotation match bug: unseen match alt

Stream: lean4

[Thomas Murrills]

I noticed that the ident match alt in the following is ignored by match, but if you "re-match" by inserting another match in the fallback case, it works:

import Lean

open Lean.Parser Term

def mweEnd : Parser := leading_parser ((Lean.Parser.ident >> " end") <|> num)

syntax (name := mweStx) "mwe_start " mweEnd : command

open Lean

elab_rules : command
| `(mweStx|mwe_start $e:mweEnd) => do
  match e with
  | `(mweEnd| $n:num) => logInfo m!"number! {n}"
  | `(mweEnd| $b:ident end) => logInfo m!"ident! {b}" -- unseen match alt
  | _ => Elab.throwUnsupportedSyntax

mwe_start 3 -- works

mwe_start b end -- error (unexpected syntax)

/- But, if we guide Lean's hand... -/

syntax (name := mweStx2) "mwe_start2 " mweEnd : command

elab_rules : command
| `(mweStx2|mwe_start2 $e:mweEnd) => do
  match e with
  | `(mweEnd| $n:num) => logInfo m!"number! {n}"
  | e => match e with
    | `(mweEnd| $b:ident end) => logInfo m!"ident! {b}"
    | _ => Elab.throwUnsupportedSyntax

mwe_start2 3 -- works

mwe_start2 b end -- works

(This issue also occurs with elab_rules:

elab_rules : command
| `(mweStx|mwe_start $n:num) => logInfo m!"number! {n}"
| `(mweStx|mwe_start $b:ident end) => logInfo m!"ident! {b}" -- unseen match alt

but I wanted to be clear that this isn't an elab_rules issue.)

Interestingly:

• " end" (or some token after ident) seems necessary for failure
• the actual parsers involved (ident, num) do not seem to matter
• the order of the match alts after match do not matter; the first always masks the second
• the order of the arguments to <|> do not matter

Note: you can see that the generated logic is wrong by printing a def:

def mweDef (e : TSyntax ``mweEnd) : Elab.TermElabM Unit := do
  match e with
  | `(mweEnd| $n:num) => logInfo m!"number! {n}"
  | `(mweEnd| $b:ident end) => logInfo m!"ident! {b}" -- unseen match alt
  | _ => logInfo "uh-oh"

#print mweDef

I haven't investigated this further; just reporting the issue for now :)

[Sebastian Ullrich]

Both sides of <|> should produce the same number of syntax trees

[Thomas Murrills]

Agh, okay—not the first time I've been bitten by <|> semantics! :)

I do wish there were some way to make this fact more discoverable, but admittedly I can't think of one with an appropriately small implementation cost, given that the need to write parsers directly like this arises rather infrequently.

(I have been wondering if we can find a way to put instance-specific documentation hovers on notation implemented by typeclasses like <|>, but that's another thread.)