Zulip Chat Archive

Stream: general

Topic: non-exhaustive match problem


view this post on Zulip Sorawee Porncharoenwase (Nov 05 2020 at 04:46):

The following code errors:

inductive type : Type
| A : type
| B  : type

inductive val : type  Type
| cA : val type.A
| cB : val type.B

inductive wrap : Type
| val :  {t : type}, (val t)  wrap

def f : wrap  
| (wrap.val val.cA) := 1
| _ := 1

with the error message:

non-exhaustive match, the following cases are missing:
f (wrap.val val.cB)

even though _ is supposed to handle that case.

There are two workarounds that I found:

  1. Change _ to (wrap.val val.cB).
  2. Change (wrap.val val.cA) to (@wrap.val type.A val.cA).

But I wonder if the problem above is expected.

view this post on Zulip Mario Carneiro (Nov 05 2020 at 05:00):

yes, this is a known issue. I forget exactly what the problem is but I think it has something to do with dependent pattern matching making it difficult to instantiate the wildcard branch where it needs to go

view this post on Zulip Bryan Gin-ge Chen (Nov 05 2020 at 05:02):

I don't think we have an open issue at https://github.com/leanprover-community/lean yet though.

view this post on Zulip Mario Carneiro (Nov 05 2020 at 05:02):

leanprover/lean#1594


Last updated: May 16 2021 at 21:11 UTC