Erased type-casing function seen as total when it's not

[gallais]

I suspect the issue is that we see {0 a : Type} and assume for coverage
checking purposes that a = Nat is a forced pattern rather than a type case.

%default total

0 oops : {0 a : Type} -> a
oops {a = Nat} = Z

boom : Void
boom = void oops