GHC Handbook

Chapter 3

The typechecker: architecture

The largest phase in GHC, and the one shaped most deliberately: it does not type-check your program so much as write down everything that must be true about it, and hand that to a separate solver.

Where this lives in the tree

The typechecker is the biggest thing in GHC by a wide margin. Around 830 of the compiler’s Notes live under GHC.Tc.* (more than the entire back end), and the files are correspondingly large.

The single most useful idea for finding your way around it is this: GHC does not check types and solve constraints at the same time. It walks your program once, writing down every fact that would have to hold for the program to be well typed, and only then hands that pile of facts to a solver. Almost every design decision in the phase follows from that split, and the next chapter is about the solver alone.

This chapter is the first half: how the walk works, and what it produces.

Why split at all

The obvious way to write a type checker (unify as you go, fail at the first mismatch) works fine for Hindley-Milner. It stops working once you have local assumptions.

f :: (a ~ Int) => a -> Int
f x = x + 1

Inside f’s body, a is Int, but only because of a constraint that arrived with the signature. And with GADTs, the assumptions available depend on which branch you are in:

data T a where
  TInt  :: T Int
  TBool :: T Bool

g :: T a -> a
g TInt  = 42       -- here, and only here, a ~ Int
g TBool = True     -- here, a ~ Bool

A checker that unifies eagerly has nowhere to put “a ~ Int, but only in this branch”. So GHC generates constraints with their context attached, and defers solving until it has the whole picture.

What gets generated

Two types carry it all. First, individual constraints:

data Ct
  = CDictCan      DictCt    -- ^ A dictionary constraint (canonical)
  | CIrredCan     IrredCt   -- ^ An irreducible constraint
  | CEqCan        EqCt      -- ^ An equality constraint (canonical)
  | CQuantCan     QCInst    -- ^ A quantified constraint
  | CNonCanonical CtEvidence

Show a is a CDictCan. a ~ Int is a CEqCan. “Canonical” means the solver has already massaged it into a normal form, a distinction that matters enormously in the next chapter and not at all here.

Second, the collection the walk produces:

data WantedConstraints
  = WC { wc_simple :: Cts              -- Unsolved constraints, all wanted
       , wc_impl   :: Bag Implication
       , wc_errors :: Bag DelayedError
       }

Note that it is a tree, not a list. wc_simple holds constraints at this level; wc_impl holds nested ones, each wrapped in an Implication that records what may be assumed locally:

data Implication
  = Implic {
      ic_tclvl :: TcLevel,        -- TcLevel of unification variables
                                  -- allocated /inside/ this implication
      ic_skols :: [TcTyVar],      -- Introduced skolems
      ic_given :: [EvVar],        -- Given evidence variables
      ic_wanted :: WantedConstraints,
      ... }

Read that as a logical implication, because that is exactly what it is: given ic_given, and with ic_skols held rigid, prove ic_wanted. The g TInt branch above becomes an implication whose given is a ~ Int.

Given and Wanted

The distinction runs through the entire phase:

data CtEvidence
  = CtGiven  GivenCtEvidence
  | CtWanted WantedCtEvidence

A Given is something you may assume: it arrived from a type signature or a GADT pattern match, and it comes with an EvVar, a variable naming the evidence you already hold. A Wanted is something you must prove, and it carries a ctev_dest: a hole to be filled in with evidence once solved.

That “evidence” is not bookkeeping. It is a real term that survives into the output: a Show a Wanted, once solved, becomes the dictionary argument you saw appear in the Core in the parser chapter’s example explorer. The typechecker is in the business of constructing programs, not merely accepting them.

Levels, skolems, and what may be unified

Two kinds of type variable exist during typechecking. A metavariable is a mutable hole standing for a type not yet known: unifying is filling it in. A skolem is rigid: it stands for a type the caller chooses, and unifying it with anything would be unsound.

Keeping this straight under nesting is what TcLevel is for, and its invariants are worth reading in full, because a startling amount of the typechecker exists to maintain them:

Note [TcLevel invariants] GHC/Tc/Utils/TcType.hs:737 
* Each unification variable (MetaTv)
  and skolem (SkolemTv)
  and each Implication
  has a level number (of type TcLevel)

* INVARIANT (KindInv) Given a type variable (tv::ki) at at level L,
                      the free vars of `ki` all have level <= L

* INVARIANTS.  In a tree of Implications,

    (ImplicInv) The level number (ic_tclvl) of an Implication is
                STRICTLY GREATER THAN that of its parent

    (SkolInv)   The level number of the skolems (ic_skols) of an
                Implication is equal to the level of the implication
                itself (ic_tclvl)

    (GivenInv)  The level number of a unification variable appearing
                in the 'ic_given' of an implication I should be
                STRICTLY LESS THAN the ic_tclvl of I
                See Note [GivenInv]

    (WantedInv) The level number of a unification variable appearing
                in the 'ic_wanted' of an implication I should be
                LESS THAN OR EQUAL TO the ic_tclvl of I
                See Note [WantedInv]
Show the rest of this Note (5 more lines) 
The level of a MetaTyVar also governs its untouchability.  See
Note [Unification preconditions] in GHC.Tc.Utils.Unify.

  See also Note [The QLInstVar TcLevel]

The payoff is (GivenInv) and (WantedInv). Together they make “may I unify this metavariable here?” answerable by comparing two integers, rather than by searching the implication tree. A metavariable from an outer level is untouchable inside an inner implication: unifying it there would smuggle a local assumption into a scope where it does not hold. This is where GHC’s “untouchable” error messages come from.

Checking and inferring

The walk itself is bidirectional. Rather than one function that infers a type, there are two modes, chosen by whether an expected type is already known:

Note [Bidirectional type checking] GHC/Tc/Gen/HsType.hs:1037 
In types, as in terms, we use bidirectional type infefence.  The main workhorse
function looks like this:

    type ExpKind = ExpType
    data ExpType = Check TcSigmaKind | Infer ...(hole TcRhoType)...

    tcHsType :: TcTyMode -> HsType GhcRn -> ExpKind -> TcM TcType

* When the `ExpKind` argument is (Check ki), we /check/ that the type has
  kind `ki`
* When the `ExpKind` argument is (Infer hole), we /infer/ the kind of the
  type, and fill the hole with that kind

That Note is about kinds, but the same ExpType machinery is used for terms. The distinction matters for higher-rank types: Check can push a polymorphic type inward, where Infer would have to guess it. It is also why moving a type signature can make a program compile.

Then it stops

At the end of the walk GHC has a WantedConstraints tree and a partially elaborated program full of evidence holes. Nothing has been solved. No Show Int has been looked up; no equality has been decomposed.

The whole of that is the next chapter.

Seeing it happen

What you wrote.

{-# LANGUAGE GADTs #-}

-- | Why the typechecker separates constraint generation from constraint solving.
--
-- Each branch of `eval` type-checks under a *different* assumption: matching on
-- `IntLit` tells GHC that `a ~ Int`, matching on `BoolLit` that `a ~ Bool`. A
-- checker that unified eagerly would have nowhere to put a fact that holds only
-- inside one alternative, so GHC records it as an implication constraint with a
-- Given, and solves later.
--
-- In the desugared Core the same facts appear as coercions: the evidence that
-- `a` and `Int` really are the same type, made into a term.
module Gadt where

data Expr a where
  IntLit  :: Int -> Expr Int
  BoolLit :: Bool -> Expr Bool
  Add     :: Expr Int -> Expr Int -> Expr Int
  If      :: Expr Bool -> Expr a -> Expr a -> Expr a
  Eq      :: Expr Int -> Expr Int -> Expr Bool

eval :: Expr a -> a
eval (IntLit n) = n
eval (BoolLit b) = b
eval (Add x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Eq x y) = eval x == eval y

-- A plain polymorphic function for contrast: no refinement anywhere, so no
-- implications are generated and the constraint set stays flat.
describe :: Show a => a -> String
describe x = "value: " ++ show x
An evaluator over a GADT. Each branch of `eval` type-checks under a different assumption, which is the whole reason this phase defers solving.

eval is the motivating example from the top of this chapter, made concrete. Turn on Full detail and look at Core (desugared): each alternative binds a co, and uses it to cast.

IntLit  co n -> n `cast` (Sub (Sym co) :: Int  ~R# a);
BoolLit co b -> b `cast` (Sub (Sym co) :: Bool ~R# a);

That co is the Given. The fact “in this branch, a is Int” started life as an implication constraint here in the typechecker, was discharged by the solver, and survives into Core as a coercion: a term, not an annotation. The elaborated program carries its own proof.

Before the Core, though, look at Typechecked itself. The output is the elaborated Haskell this chapter has been describing: bindings wrapped in AbsBinds, and EvBinds recording what the solver concluded. In the Add branch you will find [W] $dNum = GHC.Num.$fNumInt: a solved Wanted, still wearing its [W] tag, bound to the concrete instance that discharged it. And in a GADT match like eval (Eq{co EvBinds{...}} x y), the co bound inside the pattern is the Given itself, exactly where it enters scope. The Types tab is the quiet summary of the same phase: every top-level type as finally inferred, with the foralls and contexts you did not write spelled out.

describe in the same file is the contrast: no refinement, no implication, just a flat Show a Wanted that becomes a dictionary argument.

To see the walk itself rather than its result (the constraints being written down, level by level), the trace explorer runs -ddump-tc-trace on a three-line version of exactly this program: watch a GADT match become an implication.

Reading the source yourself

  1. GHC/Tc/Types/Constraint.hs before anything else. Ct, WantedConstraints, Implication and CtEvidence are the vocabulary; the rest of the phase is unreadable without them and mostly straightforward with them.
  2. GHC/Tc/Utils/TcType.hs for TcLevel and the metavariable/skolem distinction.
  3. GHC/Tc/Gen/Expr.hs for the walk itself, but only after the above.
  4. GHC/Tc/Module.hs last, for how it is all driven per module.

Be warned that GHC/Tc/Errors/Ppr.hs and Errors/Types.hs are the two largest files in the directory at around 7,000 lines each. They are error rendering, not type theory; skip them until you need to change a message.