| Copyright | (c) 2019-2020 Dmitrii Kovanikov |
|---|---|
| License | MPL-2.0 |
| Maintainer | Dmitrii Kovanikov <kovanikov@gmail.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Type.Errors.Pretty
Description
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:
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
Synopsis
- type family (l :: k1) <> (r :: k2) :: ErrorMessage where ...
- type (⊕) (l :: k1) (r :: k2) = l <> r
- type family (t :: k1) % (b :: k2) :: ErrorMessage where ...
- type (•) (t :: k1) (b :: k2) = t % b
- type family TypeError (a :: ErrorMessage) :: b where ...
- type family ToErrorMessage (t :: k) :: ErrorMessage where ...
Combinators
type family (l :: k1) <> (r :: k2) :: ErrorMessage where ... infixl 5 Source #
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 Source #
Unicode version of the <> type-level operator.
type family (t :: k1) % (b :: k2) :: ErrorMessage where ... infixr 4 Source #
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 |
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 ... Source #
Type family to convert any type to ErrorMessage.
Equations
| ToErrorMessage (t :: Symbol) = 'Text t | |
| ToErrorMessage (t :: ErrorMessage) = t | |
| ToErrorMessage t = 'ShowType t |