Moduleghc-internal-9.1003.0Haskell2010

GHC.Internal.TypeError

This module exports:

The TypeError type family, which is used to provide custom type errors. This is a type-level analogue to the term level error function.
The ErrorMessage kind, used to define custom error messages.
The Unsatisfiable constraint, a more principled variant of TypeError which gives a more predictable way of reporting custom type errors.

1 type
1 class
1 value

Packageghc-internal-9.1003.0
Exports5
LanguageHaskell2010
LicenceBSD-3-Clause
SourceTypeError.hs

datadata ErrorMessage

A description of a custom type error.

Constructors

Text Symbol
Show the text as is.
forall t. ShowType t
Pretty print the type. ShowType :: k -> ErrorMessage
ErrorMessage :<>: ErrorMessageinfixl 6
Put two pieces of error message next to each other.
ErrorMessage :$$: ErrorMessageinfixl 5
Stack two pieces of error message on top of each other.

familytype family TypeError (a :: ErrorMessage) :: b where

The type-level equivalent of Prelude.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.")

familytype family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where

A type-level assert function.

If the first argument evaluates to true, then the empty constraint is returned, otherwise the second argument (which is intended to be something which reduces to TypeError is used).

For example, given some type level predicate P' :: Type -> Bool, it is possible to write the type synonym

type P a = Assert (P' a) (NotPError a)

where NotPError reduces to a TypeError which is reported if the assertion fails.

Equations

Assert 'True _1 = ()
Assert _1 errMsg = errMsg

classclass Unsatisfiable (msg :: ErrorMessage) where

An unsatisfiable constraint. Similar to TypeError when used at the Constraint kind, but reports errors in a more predictable manner.