Pattern synonym exhaustiveness checks don't play well with EmptyCase
In #8779 (closed), mpickering added a COMPLETE
pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with EmptyCase
. Suppose I write
newtype Fin (n :: Nat) = Fin Natural -- constructor not exported
pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m -> Fin n
{-# COMPLETE FZ, FS #-}
I would very much like to be able to write
finZAbsurd :: Fin 'Z -> Void
finZAbsurd x = case x of
but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:
When checking empty case, check that at least one complete pattern set is impossible.
In this case, it would see two complete pattern sets: the built-in {Fin}
and the user-decreed {FZ, FS}
. Since neither FZ
nor FS
have matching types, we should conclude that the empty case is fine.