Skip to content

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 and fs of a : fs cannot be inferred from the right-hand side TypeError .... (check 4)
  • Overlap between the right-hand sides [] and TypeError ..., 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 _.

Edited by sheaf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information