GHC curiosities: Equality constraints in kinds
WARNING: This blog post describes an old GHC feature that no longer exists in recent versions of the compiler. See GHC Proposal #547, which lists the reasons for this feature’s removal. This post is now only of interest for historical reasons.
In GHC, many language features available at the term level can be straightforwardly promoted to the type level. For example, the following term-level function:
Can also be defined at the type level with only minor syntactic changes [1]:
There are still some GHC features that cannot yet be promoted, however. This
includes constraints, such as the class constraint Eq a
. If you try to add
a constraint to the kind of a type-level definition, such as in the example
below:
Then GHC will balk:
But as it turns out, there is one exception to this rule: equality constraints. GHC has a special case which permits kind-level equality constraints, as evidenced by the fact that this typechecks:
In this post, we will investigate why this special case exists and explore the things one can do with it.
A recap of equality constraints
In GHC, an equality constraint of the form t1 ~ t2
informs the constraint
solver that t1
must be the same type as t2
. A basic usage of equality
constraints can be seen in this example:
Although boolId1
and boolId2
technically have different type signatures,
in practice these functions are virtually identical. This is because boolId2
’s
equality constraint a ~ Bool
means that the only valid way to instantiate
a
is with Bool
. If you try to invoke boolId2 LT
, for instance, you will
get essentially the same error as if you invoked boolId1 LT
:
There are various situations where one might reach for equality constraints in their GHC toolbox. When defining class instances, for example, using equality constraints in the instance context can improve type inference. Equality constraints are also sometimes needed when defining default implementations for class methods, as explained in this section of the GHC User’s Guide.
Equality constraints in kinds… well, sort of
To a first approximation, GHC permits equality constraints in the kinds of types, just as it allows equality constraints in the types of terms. For example, GHC will accept both of these definitions:
If you have an equality constraint in a kind of a type, then any use site of that type must obey the equality. For example, suppose you were to try to do this:
As you might expect, this will produce an error message. This time, the error indicates a kind mismatch:
In this sense, equalities in the kinds of types behave much like equalities in the types of terms. I’m refraining from saying that they behave identically, however, because there are some subtle differences. Equalities in the types of terms, for instance, permit writing definitions like this one:
Unlike boolId1
and boolId2
above, in the type of boolId3
, the argument
type, a
, is technically different from the result type, Bool
. This
difference doesn’t matter so much when typechecking boolId3
, however, as
the constraint solver knows that a
should be equal to Bool
. As a result,
it’s OK to use something of type a
in a place where Bool
is expected,
and vice versa.
Unfortunately, this intuition does not carry over to equalities in the
kinds of types. If you were to write the type-level version of boolId3
:
Then this will not kind-check:
I found this difference to be pretty surprising when I first encountered it. Why don’t our intuitions about equalities apply here? There is a short answer and a long answer. (If you’d like, you can skip the long answer and proceed to the rest of the post by clicking here.)
The short explanation
GHC’s type system is simply not powerful enough at the moment to solve for
equalities at the kind level. In order to make BoolId3
above kind-check,
GHC would need some form of type-level case
that could decompose kind
equalities. Type-level case
doesn’t exist at the moment, however. We can
get close, as we will see later, but for now the full power
of case
is out of reach at the type level.
The long explanation
The difference between GHC accepting boolId3
and rejecting BoolId3
lies
in the capabilities of an intermediate language that GHC uses during
compilation. This intermediate language, called Core, differs from source
Haskell in several aspects. One difference is that there is basically
no distinction between data types and constraints.
When compiling from source Haskell to Core, GHC converts constraints into
dictionary data types. For instance, consider the Bounded
type class:
When compiled to Core, the Bounded
class would become the following
dictionary type:
Note that Bounded
’s methods have now effectively become field selectors in Core. When GHC
compiles an application of a class method, it desugars the method to a
selector applied to the appropriate dictionary value. This is best
explained by example, so let’s see how GHC takes this source Haskell program:
And compiles it to Core:
Here, the Core version of minAndMax
explicitly binds $dBounded
, a
dictionary value of type Bounded a
. Moreover, minAndMax
selects the
appropriate fields from $dBounded
using minBound
and maxBound
.
GHC also uses the dictionary-desugaring approach when compiling equality
constraints to Core. In broad strokes, here is what an a ~ b
constraint
looks like as a dictionary type:
In Core, a ~ b
is a data type which contains a ~# b
, an
unlifted equality. The exact details of how unlifted equalities work are beyond
the scope of this post. For our purposes, it suffices to know that unlifted
equalities are special values that GHC’s constraint solver makes use of to
determine when a value of one type can be safely cast to a value of a different
type. Again, this is best explained by example. Let’s see where the rubber hits
the road in the boolId3
function from before:
Here is the same function in Core:
As the Core reveals, there’s a lot happening behind the scenes in this seemingly small function! Here is a rundown of what is going on:
- First,
boolId3
extracts the payload of the$d~
dictionary value, an unlifted equality, using theeq_sel
selector. - Next, it
case
s on this unlifted equality to make sure it is evaluated strictly [2]. This unlifted equality is bound to the nameco
. - Finally,
co
is used as part of acast
expression which turnsx
from typea
to typeBool
.
Key to making all this work is case
. Without case
, we wouldn’t have been
able to define eq_sel
or boolId3
. In today’s Core, however, case
is a
feature that is exclusively available at the term level. In contrast, Core’s
sublanguage of types is rather limited, and there is no general-purpose
mechanism for pattern matching on types like what case
offers for terms.
This is why BoolId{1,2}
can be defined at the type level but BoolId3
cannot: the former can be defined without the use of case
, while
for the latter, case
is a requirement.
Why the special treatment, anyway?
Given that kind-level equality constraints are so limited, one might wonder why GHC even allows writing them in the first place. The answer is ultimately explained in this Note in GHC’s source code. The tl;dr version is that as a general rule, GHC tries to make it possible to write GADT constructors using equality constraints. For example, GHC allows writing this:
It also allows defining MkT
in the following way, which is essentially
equivalent:
There is one complication with the latter version of MkT
, however: the
DataKinds
extension. If MkT
is promoted to a type, then its kind would be
(a ~ b) => T a b
, which has a kind-level equality constraint. As it turns out, however,
one can promote MkT
to a type without running into the aforementioned issues
with type-level case
. To support examples like MkT
, GHC’s typechecker
carves out a special case for kind-level constraints that look like a ~ b
or a ~~ b
.
They’re not totally useless
Although kind-level equality constraints exist in GHC mostly due to a corner case in how
DataKinds
interacts with GADTs, there are a handful of interesting things
that can be done with them.
Faking type-level case
with type families
As mentioned before, GHC doesn’t have type-level case
. But it does have
something very close in the form of type families. Ignoring some minor
differences in semantics, type families can be thought of as a way to pattern
match types at exclusively the top level, such as in this example:
What’s more, type families offer a way to use kind-level equality constraints in a
meaningful fashion. Earlier, we failed to promote the boolId3
function to
a type synonym, but we can promote it to a type family:
Pretty cool, huh? We should be careful, however, to point out why this works.
From a certain perspective, this definition of BoolId3
is partial. This can
be seen if you examine the definition in GHCi with some additional flags
enabled:
Once again, there’s a lot happening behind the scenes that isn’t obvious at first glance:
BoolId3
matches on@Bool
, which meansBoolId3 x
will only reduce ifx
has kindBool
. GHC was able to figure this out by way of kind inference, although one could have just as well written this out explicitly asBoolId3 @Bool x = x
[3].BoolId3
also matches on@{'Eq# @Type @Bool @Bool <Bool>_N}
[4].Eq#
is the data constructor for the(~)
dictionary data type, and'Eq#
is the promoted, type-level version. Matching on this type, then, indicates that the(a ~ Bool)
kind must be witnessed with a proof thatBool
equalsBool
.- The proof that
Bool
equalsBool
is witnessed by an unlifted equality. GHCi prints this unlifted equality as<Bool>_N
.
Somewhat surprisingly, the (a ~ Bool)
equality constraint isn’t actually
required to define BoolId3
as a type family. In fact, this is a valid
alternative definition:
The advantage of including (a ~ Bool)
, however, is that it makes
it less likely that users will shoot themselves in the foot later. For instance,
this definition will kind-check:
This is because LT
has kind Ordering
, and when BoolId4
fails to match Ordering
against Bool
, it will simply become stuck. As a result, the type BoolId4 LT
will
simply never reduce.
BoolId3
, on the other hand, does
not suffer from this pitfall. If you attempt to write BoolId3 LT
, then the
typechecker will throw an Expected kind ‘Bool’, but ‘LT’ has kind ‘Ordering’
error. GHC’s constraint solver may be limited in its support for kind-level equality constraints,
but luckily, it pulls through for us in this one scenario.
Restricting GADT return types
The only other useful application of kind-level equality constraints that I am aware of involves GADTs. As far as I am aware, this trick originated in this section of the GHC User’s Guide, which demonstrates how to restrict the types that one can use in a GADT constructor’s return type. Here is the example from the User’s Guide:
Quite cleverly, the IsTypeLit a ~ True
constraint in T
’s kind limits its
data constructors such that they can only use return types T x
where x
is
either of kind Nat
or Symbol
. I haven’t yet seen this trick used outside of
this User’s Guide section, but I could envision some creative Haskellers
putting this to good use.
Other uses?
The type family and GADT use cases are, to my knowledge, the only not-totally-contrived situations where one might want to reach for a kind-level equality constraint. But then again, my imagination is somewhat limited. Perhaps you can think of a use case that I’ve overlooked?
-
Here, the kind of
Id
is written using theStandaloneKindSignatures
language extension. If you are not familiar withStandaloneKindSignatures
, you may find my earlier blog post on the topic to be informative. ↩ -
Unlike in source Haskell,
case
expressions in Core are evaluated strictly. Unlifted values cannot be inhabited by⊥
, and as a result, they must be evaluated strictly, hence the need for acase
in Core. ↩ -
In fact, if this GHC proposal is accepted, then explicitly writing out the
@Bool
part would be required. ↩ -
Note the
@{...}
syntax, which differs from normal type application syntax in that it uses curly braces instead of parentheses. This syntax indicates a visible dictionary application, which is a feature that is currently limited to Core. ↩