One of the main selling points of Haskell is that despite (or because) of its strong static type system, it frees us from the burden of having to spell out tedious type signatures everywhere.
Type inference is a blessing, but sometimes it can also be a curse. Inference too good can hinder the readability of code, because the compiler knows what the type of an identifier is even when we don’t. It’s not just readability though: correctness can be imperilled too.
As an example, consider the
Tagged type, which allows
us to attach type information to some other type.
Then we might want to define a
Person type consisting of a first
name and a last name, both of type
String, tagged by (type-level)
We can then construct values of this type:
And here is the problem. Since both fields are constructed just with
MkTagged constructor, nothing is stopping us from mixing up the
field names if we misremember the ordering:
We would wish to get a type error, but GHC happily infers that
MkTagged "Joseph" indeed has type
Tagged t String for any
thus it fits perfectly into the
We can fix this example by providing explicit type applications to
MkTagged constructor. Then, mixing up the order is a type error.
This works, but these annotations are entirely optional, and if we forget about them, we’re in trouble once again.
To summarise, the problem is that GHC can infer the type of
and due to the generality of the result, it can also unify
it with any arbitrary tag.
So the question is this: how do we stop GHC from inferring the type of
MkTagged "Joseph"? In other words, how do we enforce
that the tag must be provided by explicit type annotation?
An ambiguous smart constructor
We’re going to write a smart constructor that can only be invoked by explicit type annotation of the tag type.
What to put in the
??? hole? The idea is that we want
t in this
type to be ambiguous, in other words, it should be impossible to
t even if we know what
Tagged (???) a is. If it can’t be
inferred, then GHC will insist that we specify a type annotation at
the use site for what
t should be.
The obvious thing to plug into
??? would be
t itself, but that
doesn’t work of course, because from knowing
Tagged t a,
t can be
For example, when given a value of type
Tagged "firstName" String,
we can infer that
t must be
As always (at least this seems to be a recurring theme here on my
blog), we reach for type families to solve this problem. In
particular, we define a rather funny-looking variant of the identity
type family, which I’m going to call
The first thing that might strike you is the kind signature:
Ambiguous takes an argument of kind
k, and returns something of
j. It helps to think of these kind parameters as additional
inputs to the type family.
Ambiguous "firstName" will get stuck:
because GHC doesn’t know at which
j we want to evaluate the type
family (and indeed, in principle this choice could change the
behaviour of the type family, since in GHC, type families are not
In order to properly reduce the family, we must provide the result kind as an input, like so:
Now let us plug this type family into the type of
mkTagged, and see what happens.
Now, when GHC’s given
Ambiguous t, it can’t work out what
is. Why? Suppose we know that
Ambiguous t :: Symbol, that is, we
expect it to reduce to a symbol. That still doesn’t tell us anything
about the kind of
t! According to the kind signature of
t could be anything. Indeed, the only way to disambiguate this
is to provide the kind of
t. As the signature of
not have an explicit kind annotation on
t, the only way to provide
the kind of
t is to provide
t itself (since only visibly quantified
variables can be applied with visible type applications).
Now, the following code
results in the error:
To fix it, we now must provide type applications: