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 TypeError
.
This makes it hard if not impossible to customize type error messages.
Environment
- GHC version used: 8.10.2