## Stream: general

### Topic: non-exhaustive match problem

#### 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.

#### 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

#### 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.

#### Mario Carneiro (Nov 05 2020 at 05:02):

leanprover/lean#1594

Last updated: May 16 2021 at 21:11 UTC