haskus-utils-types-1.5: Haskus types utility modules

Safe HaskellSafe



Type-level Error



type family TypeError (a :: ErrorMessage) :: b where ... #

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: base-

data ErrorMessage where #

A description of a custom type error.


Text :: forall. Symbol -> ErrorMessage

Show the text as is.

ShowType :: forall t. t -> ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 5

Stack two pieces of error message on top of each other.

type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) :: k where ... Source #

Like: If cond t (TypeError msg)

The difference is that the TypeError doesn't appear in the RHS of the type which leads to better error messages (see GHC #14771).

For instance: type family F n where F n = If (n <=? 8) Int8 (TypeError (Text ERROR))

type family G n where G n = Assert (n <=? 8) Int8 (Text ERROR)

If GHC cannot solve `F n ~ Word`, it shows: ERROR If GHC cannot solve `G n ~ Word`, it shows: can't match .. with Word


Assert True val msg = val 
Assert False val msg = TypeError msg