TypeError and GADT pattern matching exhaustiveness
data D a where C1 :: D Int C2 :: D Char type family Elem x list where Elem x ' = 'False Elem x (x ': as) = 'True Elem x (y ': as) = Elem x as foo :: Elem a '[Int] ~ 'True => D a -> () foo C1 = ()
Here GHC correctly determines that the pattern matching is exhaustive. But if the first case of the type family is changed to
Elem x ' = TypeError ('Text "oops")
then GHC no longer thinks it's exhaustive.
This seems to be the case with any empty type family, not just
This makes it hard if not impossible to customize type error messages.
- GHC version used: 8.10.2