Typeclass inference fails with nested pattern matching

Stream: general

[Seul Baek]

Lean has no problems with

def foo : nat → unit
| 0 := ()
| (k+1) :=
  if (0 < k)
  then ()
  else ()

But if I change the first match case

def bar : nat → unit
| 0 :=
  match 0 with
  | _ := ()
  end
| (k+1) :=
  if (0 < k)
  then ()
  else ()

Then Lean suddenly can't decide 0 < k. But if you swap the match case order

def baz : nat → unit
| (k+1) :=
  if (0 < k)
  then ()
  else ()
| 0 :=
  match 0 with
  | _ := ()
  end

Then it works again. Apparently Lean doesn't like nested pattern matching, but it's a bit strange that this should affect typeclass inference or be sensitive to the match case order. Any thoughts on what's going on here?

[Mario Carneiro]

I think the main problem there is that the type of 0 in the match is not known

[Seul Baek]

If I modify bar to

def bar' : nat → unit
| (k+2) :=
  match k with
  | _ := ()
  end
| (k+1) :=
  if (0 < k)
  then ()
  else ()
| _ := ()

The problem still persists, so I think it's likely something else

[Mario Carneiro]

It's some race condition, I think. I've got it down to this:

set_option trace.class_instances true
set_option pp.all true
def baz : nat → unit
| 0 := match (0:ℕ) with _ := () end
| ((k:ℕ)+1) :=
  @ite (@has_lt.lt _ _ (0:ℕ) (k:ℕ)) (_) unit () ()

[Mario Carneiro]

filling any of the underscores makes it work

[Seul Baek]

Thanks. I guess the rule of thumb is to supply more explicit type information whenever something like this happens