Haskus.Utils.Types.Error

Type-level Error

Documentation

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-4.9.0.0

data ErrorMessage where

A description of a custom type error.

Constructors

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 ...

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

Equations

Assert True val msg = val

Assert False val msg = TypeError msg