### Overview

Custom type errors are a great way to improve the usability of Haskell libraries that utilise some of the more recent language extensions. Yet anyone who has written or used one of these libraries will know that despite the authors’ best efforts, there are still many occasions where a wall of text jumps out, leaving us puzzled as to what went wrong.

This post is about one particular class of such errors that have been troubling users of many modern Haskell libraries: stuck type families.

The following type error perfectly illustrates the problem. It is an actual error reported on the issue tracker of the generic-lens library.

Can you spot the problem? Even if you know what to look for, it takes a good few seconds to locate the culprit. The goal of this post is to turn the above into the following:

How could we possibly identify a lack of `Generic`

instance from the
above? Let us have a closer look at that large type error. It is a
nested chain function of calls, such as `Snd`

and `Interesting`

, which
are type families leaking out of the library’s implementation. The
reason we see these type families (as opposed to the result they
evaluate to), is because the computation is *stuck*. The culprit is
the `Rep Text`

part somewhere in the middle.

It turns out that `Rep`

is an associated type family of the `Generic`

class:

Thus, the reason `Rep Text`

is not defined is that `Text`

has no
`Generic`

instance. Clearly, it’s unreasonable to expect users to keep
such implementation details in mind and hunt for unreduced occurrences
of `Rep`

in their type errors to find out what the issue is!

Yet, reporting this is not so easy. To explain why, we need to understand the behaviour of type families.

As things stand today, the associated family `Rep`

is not actually
connected to the `Generic`

class as far as the type checker is
concerned. This is why unreduced occurrences will not result in error
messages mentioning anything about `Generic`

in the first place.
Constrained type families offer a solution to this problem, but
they are not (yet) implemented in GHC.

## Type family evaluation semantics

The reduction of type families is driven by the constraint solver. To the best of my knowledge, there is no formal specification for their semantics, so I’m not going to attempt to give a comprehensive account here either. Instead, let us just make some key observations about how type families reduce.

A type involving a type family is said to be *stuck* if none of the
type family’s equations can be selected for the provided
arguments. Since `Text`

s have no `Generic`

instance, there is
consequently no `Rep Text`

instance defined either. Thus, `Rep Text`

is stuck.

How does “stuckness” propagate up a chain of function calls? Consider the following type family:

No matter what we pass in as the argument, the single equation will
always match. This means that even if we pass in a stuck type, such as
`Rep Text`

, the equation can reduce to the right hand side (and get
stuck afterwards):

In other words, we can think of `Foo`

as a type family that’s “lazy”
in its argument. Now consider the `Bar`

type family:

Here, we first check if the argument is `Maybe`

, in which case `Maybe`

is returned, otherwise we pick the second equation. Perhaps
surprisingly, `Bar`

behaves the same as `Foo`

:

The two equations of `Bar`

*agree* with each other, because the first
one is a substitution instance of the second. GHC recognises this, and
decides that it is safe to drop the first equation in favour of the
second one.

We can of course write disagreeing equations:

This time, notice that the first equation is not a substitution instance of the second: it returns something other than the argument.

GHC won’t optimise this case away anymore, and now instance matching
will have to consider both equations. A given equation matches, if the
argument unifies with the pattern, and is apart from all of the preceding
patterns (i.e. doesn’t match any of them).
The important thing here is that a stuck type is *not* apart from any
other type, but neither does it match any other type. This means that

`FooBar`

gets stuck just when its argument does. We can think of
`FooBar`

as a type family that is “strict” in its argument.

If we pass in a non-stuck value, evaluation proceeds as normal:

Since `Maybe`

is apart from `T1`

(they are different ground types), and
it unifies with the catch-all pattern `a`

.

So, if a type family that inspects its argument is given a stuck type,
then the resulting type will be stuck itself. Notice that we can’t
proceed any further: there is no way to detect if the argument was
stuck or not. This is why the type error above is so impenetrable.
If we ignore our argument like `Foo`

does, then it just slips by, but
if we try to do something with it like `FooBar`

does, we get stuck.

Of course, I wouldn’t have written down all of these low-level details about type family reduction if they didn’t lead to a solution!

## Custom type errors

The mechanism of custom type errors is quite simple. The constraint
solver proceeds normally, reducing all type family equations and
solving all type class instances. If at the end, there are any
constraints of the form `TypeError ...`

, then the payload of the error
gets printed, otherwise any unsolved constraints are reported.

As an example

yields

even though `10`

clearly doesn’t have type `()`

.

We want to produce a custom type error when the `Rep`

type family gets
stuck, and we’d like to continue normally otherwise. As discussed
above, there is no way to branch on whether a type family is stuck or
not.

However, we now have all the necessary pieces: all we need to do is
to make sure that when `Rep`

gets stuck, we leave a `TypeError`

in the
residual constraints. To do this, we’re going to wrap the call to `Rep`

in
another type family, which will get stuck just when `Rep`

is stuck. When
`Rep`

reduces, our wrapper reduces too. The additional piece is that
the wrapper will also hold a type error as its argument, which will
reside in the unsolved constraint in the stuck case, but disappear otherwise.

`Break`

is the wrapper family. It takes a constraint, which will be
our type error. Then it forces its argument by testing against
`T1`

. Note that in both equations, the type family reduces to the
trivial constraint `()`

, but in the first case, we use `((), ())`

(a
tuple of two trivial constraints) to ensure that the equations
don’t optimise away, like they did with `Bar`

.

Finally, we introduce a type family to construct a custom error message:

Now, consider what happens when we call `Break`

with the stuck
argument `Rep Text`

:

the type gets stuck, with a `TypeError`

inside! However, when
called with a type where `Rep`

is defined, such as `Bool`

, the type reduces
to the unit constraint, no mention of the type error.

And with this, we can report errors for any stuck type family.

yields

# Conclusion

Using this technique, we can place custom type errors right where our stuck type families are, and provide more contextual information about what went wrong. We can even generalise the above to the following type family:

which we can use at any point in a computation, not just in
constraints. `Assert`

takes a type error, a potentially stuck
computation, and a value. If the computation is stuck, then the custom
error is presented, otherwise the value is passed through without any
errors. Here, strictness is forced by the same `T1`

trick, but this
time, to ensure that the right hand sides are also different, we
return the `Any`

type family in the first case.