HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Moduletype-errors-pretty-0.0.1.2Haskell2010

Type.Errors.Pretty

SPDX-License-Identifier: MPL-2.0 Maintainer: Dmitrii Kovanikov kovanikov@gmail.com Kowainik xrom.xkov@gmail.com

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
  • 2 types

Combinators

4 declarations
familytype family (<>) (l :: k1) (r :: k2) :: ErrorMessage where
#

Append two types automatically converting them to corresponding ErrorMessage constructors.

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

Equations

typetype (⊕) (l :: k1) (r :: k2) = l <> r
#

Unicode version of the <> type-level operator.

familytype family (%) (t :: k1) (b :: k2) :: ErrorMessage where
#

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

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

Equations

typetype (•) (t :: k1) (b :: k2) = t % b
#

Unicode version of the % type-level operator.

Reexports from GHC.TypeLits

1 declaration
familytype 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.")

Helper internal type families

1 declaration