Bug in syntax match

[digama0]

Minimized from an issue reported to mathlib4 on Zulip.

It appears that the presence of the 1 case below is causing the 2 case to be skipped.

import Lean
open Lean

syntax (docComment)? "foo" term : command

def foo1 : Syntax → Nat
  -- | `($[$_]? foo !$_) => 1
  | `(foo -$_) => 2
  | _ => 0

def foo2 : Syntax → Nat
  | `($[$_]? foo !$_) => 1
  | `(foo -$_) => 2
  | _ => 0

#eval foo1 (Unhygienic.run `(foo -x)) -- 2
#eval foo2 (Unhygienic.run `(foo -x)) -- 0

Here are the resulting functions:

def foo1 : Syntax → Nat :=
fun x =>
  let_fun __discr := x;
  if Syntax.isOfKind __discr `command_Foo_ = true then
    let_fun __discr_1 := Syntax.getArg __discr 0;
    if Syntax.matchesNull __discr_1 0 = true then
      let_fun __discr_2 := Syntax.getArg __discr 1;
      let_fun __discr_3 := Syntax.getArg __discr 2;
      if Syntax.isOfKind __discr_3 `term-_ = true then
        let_fun __discr := Syntax.getArg __discr_3 0;
        let_fun __discr := Syntax.getArg __discr_3 1;
        2
      else
        let_fun __discr := Syntax.getArg __discr 2;
        0
    else
      let_fun __discr_2 := Syntax.getArg __discr 0;
      let_fun __discr_3 := Syntax.getArg __discr 1;
      let_fun __discr := Syntax.getArg __discr 2;
      0
  else
    let_fun __discr := x;
    0

def foo2 : Syntax → Nat :=
fun x =>
  let_fun __discr := x;
  if Syntax.isOfKind __discr `command_Foo_ = true then
    let_fun __discr_1 := Syntax.getArg __discr 0;
    let yes := fun x =>
      let_fun __discr_2 := Syntax.getArg __discr 1;
      let_fun __discr_3 := Syntax.getArg __discr 2;
      if Syntax.isOfKind __discr_3 `term!_ = true then
        let_fun __discr := Syntax.getArg __discr_3 0;
        let_fun __discr := Syntax.getArg __discr_3 1;
        1
      else
        let_fun __discr := Syntax.getArg __discr 2;
        0;
    if Syntax.isNone __discr_1 = true then yes ()
    else
      let_fun __discr_2 := __discr_1;
      if Syntax.matchesNull __discr_2 1 = true then
        let_fun __discr := Syntax.getArg __discr_2 0;
        yes ()
      else
        let_fun __discr_3 := __discr_1;
        let_fun __discr_4 := Syntax.getArg __discr 0;
        if Syntax.matchesNull __discr_4 0 = true then
          let_fun __discr_5 := Syntax.getArg __discr 1;
          let_fun __discr_6 := Syntax.getArg __discr 2;
          if Syntax.isOfKind __discr_6 `term-_ = true then
            let_fun __discr := Syntax.getArg __discr_6 0;
            let_fun __discr := Syntax.getArg __discr_6 1;
            2
          else
            let_fun __discr := Syntax.getArg __discr 2;
            0
        else
          let_fun __discr_5 := Syntax.getArg __discr 0;
          let_fun __discr_6 := Syntax.getArg __discr 1;
          let_fun __discr := Syntax.getArg __discr 2;
          0
  else
    let_fun __discr := x;
    0

The foo2 code is not correct, since it starts with if Syntax.isNone __discr_1 = true then yes () so the input foo -x would go into the yes () branch, but there is no 2 branch in there, which is why we get a 0 in the foo2 case instead of the expected 2.