Zulip Chat Archive

Stream: general

Topic: Typeclass inference fails with nested pattern matching


view this post on Zulip Seul Baek (Feb 20 2019 at 04:49):

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?

view this post on Zulip Mario Carneiro (Feb 20 2019 at 05:04):

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

view this post on Zulip Seul Baek (Feb 20 2019 at 05:08):

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

view this post on Zulip Mario Carneiro (Feb 20 2019 at 05:13):

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 () ()

view this post on Zulip Mario Carneiro (Feb 20 2019 at 05:14):

filling any of the underscores makes it work

view this post on Zulip Seul Baek (Feb 20 2019 at 05:31):

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


Last updated: May 15 2021 at 23:13 UTC