Description

Type-level Error

Synopsis

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

Equations

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