Typechecker complains that it can't match on erased argument when it actually can

[buzden]

Steps to Reproduce

Arguments with quantity 0 can be matched when they have the only constructor in the current context. E.g. this successfully typechecks:

data Y : Bool -> Type where
  T : Y True
  F : Y True -> Y False

a : (0 _ : Y True) -> Unit
a T = ()

b : (0 _ : Y False) -> Unit
b (F T) = ()

You can do this when type index is more complex:

data X : Nat -> Type where
  N : X Z
  C : X n -> X (S n)

g : (0 _ : X 0) -> Unit
g N = ()

f : (0 _ : X 1) -> Unit
f (C x) = ()

You can match all this deeply with unrestricted quantity and everything typechecks total, prooving that there is only one constructor to match:

total
h' : (_ : X 1) -> Unit
h' (C N) = ()

But now match deeply still with quantity 0:

h : (0 _ : X 1) -> Unit
h (C N) = ?foo

Expected Behavior

Typechecks fine

Observed Behavior

Y:17:6--17:7
 15 | 
 16 | h : (0 _ : X 1) -> Unit
 17 | h (C N) = ?foo
           ^

Additional observation

If you make argument n to be unrestricted in the constructor C all of the sudden function h starts to be typecheckable.

[andrevidela]

This is an example of "uninformative matching" right?

[buzden]

This is an example of "uninformative matching" right?

I'm not aware of this term. I'd call them "non-decision matching", because matching on erased values with a single constructor like in the examples above still can bring erased subproofs into the context or unify variables with something, so such matching brings information into the context, probably it's unfair to call this "uninformative"

[dunhamsteve]

Possibly related to #2513, which calls them irrefutable. (That issue is about let though.)