Notes for Authors of Type Checker Plugins
As of 52fc2719, a type checker plugin can extend GHC in exactly one way: the GHC constraint solver occasionally gives each plugin a chance to modify the constraints it is working on.
This page summarizes some main ideas of the constraint solver. I wrote this specifically when I was investigating what Derived constraints are, so the summary currently focuses on those and related concepts.
[The Note
references below are accurate as of writing
(GHC commit 52fc2719).]
The Constraint Solver
The constraint solver manages two groups of constraints
- a set of inert constraints that satisfies several invariants, which in particular ensure that each is "independent" of the others and/or marked as "invalid" (for some definition of "independent" and "invalid")
- a work list of constraints not yet in the inert set
Each iteration of the loop uses the inerts to simplify the next work item until it is also inert (maybe even solved) and then kicks-out any formerly-inert constraint back onto the work list if the new inert can simplify it. This repeats until the work list is empty. If no contradictory or unsatisfiable constraints were found, the unique solution was found. Otherwise, GHC reports to the user those it judges to be helpful.
Evidence
The constraint solver maintains evidence, A constraint flavor is one of
-
W
"Wanted": the user program wants the constraint's evidence from the solver -
G
"Given": the user program gives the constraint's evidence to the solver -
D
"Derived": the user program neither wants nor gives the constraint's evidence
(See Note [Constraint flavours]
.)
Intuitions:
- a constraint is essentially a type that inhabits the kind
Constraint
(egOrd Int :: Constraint
,(a ~ b) :: Constraint
, etc) - a constraint's evidence inhabits that type
- a type class is a record type that its dictionaries inhabit
- the dictionary fields are the methods and the superclass dictionaries
- an instance is a function from its context's dictionary to its head's dictionary
- Given evidence originates from invisible arguments in patterns
- Wanted evidence ends up as invisible arguments in expressions
- Wanted evidence is a tree of built-in axia and top-level instance functions applied to Given evidence
Derived Constraints
Derived constraints have one purpose: improvement of genuine constraints
by discovering equalities that must be satisfied in every possible solution
of these Wanteds in the scope of these Givens.
Deriveds are thus used to find and apply most general unifiers during constraint solving.
(See Note [The improvement story and derived shadows]
.)
(Aside: Derived CDictCan
s and Derived CFunEqCan
s are therefore only worth the trouble
because they may interact with other Deriveds to yield Derived CTyEqCan
s.)
The flavors W
G
D
would suffice for the solver.
However, W
and D
share enough semantics
and implementation efficiency matters enough
to justify an additional hybrid flavor:
-
WD
AW
that can split (once) into aW
and an initially-identicalD
A D
arises either directly (eg from a fundep) or from the on-demand splitting of a WD
.
(See Note [Constraint flavours]
.)
When does a WD
split? That's determined by rewriting.
Rewriting
The equality constraints in the inert set define the inert substitution, which rewrites work items by replacing each type variable by the type to which it is equal. As in unification, this substitution propagates so-called "positive information": what the type variable is, as opposed to what it is not.
can-rewrite
relation
The Whether an equality constraint is allowed to rewrite another constraint
depends on the flavors and roles.
(See Definition [Can-rewrite relation]
in Note [inert_eqs: the inert equalities]
.)
In terms of just flavors
-
G
can-rewrite
*
-
D
can-rewrite
D
Wanteds are not allowed to rewrite Wanteds because it results in very unhelpful error messages.
(See Note [Wanteds do not rewrite Wanteds]
.)
In additon to its flavor, an equality constraint also has a role, which is the equality relation it uses. It's one of
-
N
"Nominal": judgemental type equality (as in atype
synonym declaration) -
R
"Representational": representational equality (as in anewtype
declaration)
In terms of just roles
-
N
can-rewrite
*
-
R
can-rewrite
R
The D/R
constraints are odd (see Note [Deriveds do rewrite Deriveds]
),
so the actual rules are
-
G/N
can-rewrite
*/*
-
G/R
can-rewrite
*/R
-
D/N
can-rewrite
D/N
-
WD/N
can-rewrite
D/N
WD
s
Splitting Once a WD
work item has been made inert, one of two things happens:
- it does not split and remains an inert
WD
- it is split into an inert
W
and a newD
work item
It is split only if the inerts will usefully rewrite the new D
"shadow".
That is, if
- an inert equality
can-rewrite
the shadow - that equality maps one of the shadow's "interesting" free variables (for some definition of "interesting")
Splitting WD
s
- makes the solver more complete (cf improvement)
- preserves inert set invariants related to
can-rewrite
that ensure the solver terminates
TODO
I plan to migrate more of my notes onto this wiki page.
- Canonical constraints
- Levels (untouchables)
- Flattening
- Zonking
- Coercions
- Ambiguity checks
- Pattern checks (accessibility/reachability)
Please contact me with suggestions: nicolas.frisby@gmail.com.