Interactive case split misses pattern which requires unification

[eayus]

Given the following module:

module Test

data T : Nat -> Type where
    A :                T Z
    B : (0 n : Nat) -> T n

f : T Z -> ()
f t = ?h1

Case splitting on the variable t in function f creates the following clauses:

f : T Z -> ()
f A = ?h1_0

Which is not covering, as the case B Z is also valid value for T Z.

This does not seem to be related to erasure, as adding/removing quantities does not change the result. Making the constructor B take an implicit natural number results in the cases being generated correctly. Therefore it seems the case splitter is struggling when it must unify the explicit paramter n with Z

[dunhamsteve]

This is also an issue if the n is not erased:

data T : Nat -> Type where
    A :              T Z
    B : (n : Nat) -> T n

f : T Z -> ()
f x = ?h1