TypeError's interaction with type family injectivity
Let's say I have the following Haskell code, using TypeFamilyDependencies
:
data FieldK
data Field (f :: FieldK)
type family FieldToFieldKList (fs :: [Type]) = (r :: [FieldK]) | r -> fs where
FieldToFieldKList '[] = '[]
FieldToFieldKList (Field f : fs) = f : FieldToFieldKList fs
FieldToFieldKList (a : fs) = TypeError (Text "Must be a Field: " :<>: ShowType a)
This is currently thrice rejected by GHC:
-
TypeError
is a type family, and injective type family equations cannot have type family applications on their right-hand side (Verifying injectivity annotation note, check 3) - Type variables
a
andfs
ofa : fs
cannot be inferred from the right-hand sideTypeError ...
. (check 4) - Overlap between the right-hand sides
[]
andTypeError ...
, because type family applications pre-unify with everything (check B2)
Without the third (the TypeError
) clause, GHC accepts this type family definition as injective.
My question is whether these three rejection reasons can be alleviated by the fact that the RHS in question is a TypeError
. The idea being, if somewhere inside a type we arrive at a TypeError _
, this will lead to a type error anyway, so we won't try to solve any further type equations. So it shouldn't cause any problems if we could derive inconsistent equations from type family applications that reduce to TypeError _
.