|
|
## Custom Type Errors
|
|
|
|
|
|
|
|
|
This page outlines the design for a GHC feature to provide support for user-specified type errors.
|
|
|
The main idea was presented by Lennart Augustsson at the 2015 Haskell Symposium in Vancouver BC.
|
|
|
|
|
|
### The Problem
|
|
|
|
|
|
|
|
|
When designing EDSLs in Haskell, it is useful to have something like `error` at the type level.
|
|
|
In this way, the EDSL designer may show a type error that is specific to the DSL, rather than the standard GHC type error.
|
|
|
|
|
|
|
|
|
For example, consider a type classes that is not intended to be used with functions, but the EDSL user accidentally used
|
|
|
it at a function type, perhaps because they missed an argument to some function. Then, instead of getting a the standard
|
|
|
GHC message about a missing instance, it would be nicer to emit a more friendly message specific to the EDSL.
|
|
|
|
|
|
|
|
|
Similarly, the reduction of a type-level function may get stuck due to an error, at which point it would be nice to
|
|
|
report an EDSL specific error, rather than a generic error about an ambiguous type or something.
|
|
|
|
|
|
### A Solution
|
|
|
|
|
|
|
|
|
One way to solve the above problem is by adding a single uninterpreted type-function as follows:
|
|
|
|
|
|
```
|
|
|
typefamilyTypeError(msg ::ErrorMessage):: k
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that `TypeError` is polymorphic in the kind of result it returns, so it may be used in any context. In this respect it resembles to polymorphic value `error`.
|
|
|
The intention is that users will never define instances of `TypeError`, so one may think of it as closed type family with no equations. In other words, `TypeError`
|
|
|
will never evaluate to anything, and it is basically very similar to the polymorphic type-level value `Any`, which is already present in GHC.
|
|
|
|
|
|
|
|
|
The kind `ErrorMessage` is a small DSL for constructing error messages, and may be defined using a promoted datatype:
|
|
|
|
|
|
```
|
|
|
data{-kind-}ErrorMessage=TextSymbol-- Show this text as is| forall t.ShowType t -- Pretty print a type|ErrorMessage:<>:ErrorMessage-- Put two chunks of error message next to each other|ErrorMessage:$$:ErrorMessage-- Put two chunks of error message above each other
|
|
|
```
|
|
|
|
|
|
### Examples
|
|
|
|
|
|
|
|
|
Here are some examples of how one might use these:
|
|
|
|
|
|
```
|
|
|
instanceTypeError(Text"Cannot 'Show' functions.":$$:Text"Perhaps there is a missing argument?")=>Show(a -> b)where
|
|
|
showsPrec =error"unreachable"
|
|
|
```
|
|
|
|
|
|
|
|
|
The resulting error message from GHC is:
|
|
|
|
|
|
```wiki
|
|
|
Cannot 'Show' functions.
|
|
|
Perhaps there is a missing argument?
|
|
|
In the expression: show id
|
|
|
In an equation for ‘f’: f = show id
|
|
|
```
|
|
|
|
|
|
|
|
|
Similarly, one may use the same sort of technique in type family instances;
|
|
|
|
|
|
```wiki
|
|
|
type family F a where
|
|
|
F Int = Bool
|
|
|
F Integer = Bool
|
|
|
F Char = Int
|
|
|
F a = TypeError (Text "Function F does not work for type " :<>:
|
|
|
ShowType a :<>: Text "." :$$:
|
|
|
Text "It works only on integers and characters.")
|
|
|
```
|
|
|
|
|
|
|
|
|
The resulting error message from GHC is:
|
|
|
|
|
|
```wiki
|
|
|
Function F does not work for type [Int].
|
|
|
It works only on integers and characters.
|
|
|
In the expression: undefined
|
|
|
In an equation for ‘f’: f = undefined
|
|
|
```
|
|
|
|
|
|
### Implementation
|
|
|
|
|
|
|
|
|
The implementation in GHC is fairly straight-forward:
|
|
|
|
|
|
1. When we are reducing a type function, and we notice that the RHS is of the form `TyperError msg :: k`, then
|
|
|
we stop reducing the type function, and instead we emit a new wanted constraint `TypeError msg :: Constraint`.
|
|
|
Since there is no way to solve such constraints, this constraint is eventually reported as an error, and will
|
|
|
be rendered using a custom pretty printer. (QUESTION: Should we mark the `TypeError` constraint as unsolvable straight away?).
|
|
|
|
|
|
1. We add custom pretty printing for unsolved constraints of the form `TypeError msg :: Constraint`.
|
|
|
The custom pretty printing code examines `msg` and interprets it using the standard pretty printing combinators.
|
|
|
|
|
|
1. When interpreting `msg` it is useful to evaluate type level functions that we encounter along the way.
|
|
|
This allows the programmer to use type-level functions to construct the `msg`. OTOH, the types within
|
|
|
`ShowType` are printed as is, without evaluating function any more than usual.
|
|
|
|
|
|
1. `TypeError msg :: k` where `k` is not constraint is printed simply as `(type error)`. The reason for this
|
|
|
|
|
|
> >
|
|
|
> > is that on occasion such types may appear in other parts of the error message and we don't want to print the
|
|
|
> > error multiple times, or in its ugly DSL form.
|
|
|
|
|
|
### Alternative Design
|
|
|
|
|
|
|
|
|
It is our intention that `TypeError` will usually in the RHS of a type-level function defintion,
|
|
|
or as the sole participant in the context of a class `instance`. It is probably not useful to write `TypeError` in
|
|
|
a user-defined signature or a datatype declaration, but it also does not appear to be harmful to do so---at least
|
|
|
not any more harmful than any other partial type-level function.
|
|
|
|
|
|
|
|
|
Instead of using the type function `TypeError`, we could ad special language syntax for error-reporting class instances
|
|
|
and type-family instances. This seems like a bit heavy-weight, and it is not clear that it buys us much. Also, we'd
|
|
|
have to think of more syntax and implement it. |