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