Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Type-level Error
Synopsis
- type family TypeError (a :: ErrorMessage) :: b where ...
- data ErrorMessage
- type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) :: k where ...
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 #
A description of a custom type error.
Text Symbol | Show the text as is. |
ShowType t | Pretty print the type.
|
ErrorMessage :<>: ErrorMessage infixl 6 | Put two pieces of error message next to each other. |
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 `Assert...` with Word