Match inference not working over two variables

Stream: new members

[Jonathan Lacombe]

I am noticing match inference not working when matching on two variables and when at least one match has a filled/covered argument thats a Nat. See example below

inductive Color
  | red (n: Nat)
  | green
  | blue
  | yellow
  | orange

def both_red_or_either_zero (c: Color) (d: Color): Bool :=
  match c, d with
  | .red _, .red _  => true
  | .red 0, _       => true
  | _,      .red 0  => true
  | _,      _       => false

def match_double (c: Color) (d: Color) :=
  if _: both_red_or_either_zero c d then
    match c, d with
    | .red _, .red _  => "case 1"
    | .red 0, _       => "case 2"
    | _,      .red 0  => "case 3"
  else
    "case default"

I've seen it work in the Nat case like above, but if I switched the argument type to be (n: Number) instead, defined like so:

inductive Number where
  | zero
  | one
  | two

then there are no issues with the inference.

Am I missing something or is this a bug?