non-exhaustive match problem

Stream: general

[Sorawee Porncharoenwase]

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.

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

leanprover/lean#1594