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.
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.
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
Note [Constraint flavours].)
- a constraint is essentially a type that inhabits the kind
Ord 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 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.
[The improvement story and derived shadows].)
CDictCans and Derived
CFunEqCans are therefore only worth the trouble
because they may interact with other Deriveds to yield Derived
D would suffice for the solver.
D share enough semantics
and implementation efficiency matters enough
to justify an additional hybrid flavor:
Wthat can split (once) into a
Wand an initially-identical
D arises either directly (eg from a fundep) or from the on-demand splitting of a
Note [Constraint flavours].)
When does a
WD split? That's determined by 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.
Whether an equality constraint is allowed to rewrite another constraint
depends on the flavors and roles.
Definition [Can-rewrite relation] in
Note [inert_eqs: the inert equalities].)
In terms of just flavors
Wanteds are not allowed to rewrite Wanteds because it results in very unhelpful error messages.
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 a
R"Representational": representational equality (as in a
In terms of just roles
D/R constraints are odd (see
Note [Deriveds do rewrite Deriveds]),
so the actual rules are
WD work item has been made inert, one of two things happens:
- it does not split and remains an inert
- it is split into an inert
Wand a new
It is split only if the inerts will usefully rewrite the new
That is, if
- an inert equality
- that equality maps one of the shadow's "interesting" free variables (for some definition of "interesting")
- makes the solver more complete (cf improvement)
- preserves inert set invariants related to
can-rewritethat ensure the solver terminates
I plan to migrate more of my notes onto this wiki page.
- Canonical constraints
- Levels (untouchables)
- Ambiguity checks
- Pattern checks (accessibility/reachability)
Please contact me with suggestions: email@example.com.