Type.Errors.Pretty

This module provides type-level functions and operators to make the job of writing text of custom type errors easier. The motivation behind using custom type errors is described in detail in the following blog post:

• A story told by Type Errors

If you want to write the text of a custom error message, you need to use constructors of the ErrorMessage data type. But this gets messy and inconvenient pretty quickly. Consider the following examples:

type MessageText (e1 :: k) (e2 :: k) (es :: [k]) =
       'Text "You require the following two effects from your computation:"
 ':$$: 'Text ""
 ':$$: 'Text "    '" ':<>: 'ShowType e1 ':<>: 'Text "' and '" ':<>: 'ShowType e2 ':<>: 'Text "'"
 ':$$: 'Text ""
 ':$$: 'Text "However, your monad is capable of performing only the following effects:"
 ':$$: 'Text ""
 ':$$: 'Text "    " ':<>: 'ShowType es

Using combinators from this library, you can define error messages in a simpler way:

type MessageText (e1 :: k) (e2 :: k) (es :: [k])
    = "You require the following two effects from your computation:"
    % ""
    % "    '" <> e1 <> "' and '" <> e2 <> "'"
    % ""
    % "However, your monad is capable of performing only the following effects:"
    % ""
    % "    " <> es

If you prefer, you can use unicode operators to contstruct messages:

type MessageText (e1 :: k) (e2 :: k) (es :: [k])
    = "You require the following two effects from your computation:"
    • ""
    • "    '" ⊕ e1 ⊕ "' and '" ⊕ e2 ⊕ "'"
    • ""
    • "However, your monad is capable of performing only the following effects:"
    • ""
    • "    " ⊕ es

Combinators

type family (l :: k1) <> (r :: k2) :: ErrorMessage where ... infixl 5

Append two types automatically converting them to corresponding ErrorMessage constructors.

>>> :kind! "Integer values have type: " <> Int
"Integer values have type: " <> Int :: ErrorMessage
= 'Text "Integer values have type: " ':<>: 'ShowType Int

Equations

l <> r = ToErrorMessage l :<>: ToErrorMessage r

type (⊕) (l :: k1) (r :: k2) = l <> r infixl 5

Unicode version of the <> type-level operator.

type family (t :: k1) % (b :: k2) :: ErrorMessage where ... infixr 4

Append two types on top of each other automatically converting them to corresponding ErrorMessage constructors.

>>> :kind! "Expecting value of type: " % "   " <> Integer
"Expecting value of type: " % "   " <> Integer :: ErrorMessage
= 'Text "Expecting value of type: "
  ':$$: ('Text "   " ':<>: 'ShowType Integer)

Equations

t % b = ToErrorMessage t :$$: ToErrorMessage b

type (•) (t :: k1) (b :: k2) = t % b infixr 4

Unicode version of the % type-level operator.

Reexports from GHC.TypeLits

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

Helper internal type families

type family ToErrorMessage (t :: k) :: ErrorMessage where ...

Type family to convert any type to ErrorMessage.

Equations

ToErrorMessage (t :: Symbol) = 'Text t

ToErrorMessage (t :: ErrorMessage) = t

ToErrorMessage t = 'ShowType t