Lesson 7.4 — Constraint-based inference: HM(X) and OutsideIn(X)¶

Techniques: HM(X) — Hindley–Milner parameterized by a constraint system X, with inference split into constraint generation and constraint solving (Odersky, Sulzmann & Wehr 1999 [OSW99]; the presentation of Pottier & Rémy [PR05]); OutsideIn(X) — GHC's inference with local assumptions (GADTs, type families): implication constraints, touchable variables, and no guessing (Vytiniotis, Peyton Jones, Schrijvers & Sulzmann 2011 [VPJSS11]) · Pebble implements: Pebble's numeric literals are HM(X) with X = "is int or float" — the independent oracle tools/course/lib/pebble_infer.py generates and then solves exactly these constraints; the C++ inferTypes solves them eagerly (Lesson 7.6) · Drills: — (see §9) · Prerequisites: Lessons 7.1–7.3 · Time: 5 hours

Every extension of ML's type system — records, overloading, subtyping, units of measure, type classes, Pebble's two-way literals — used to come with its own inference algorithm and its own proofs. HM(X) turns this around: write inference once, as generating constraints and solving them, and plug in the constraint language X; if X satisfies a few conditions, soundness and principal types come for free. GHC then met constraints that HM(X) cannot handle — facts that are true only inside a pattern match on a GADT — and OutsideIn(X) is its answer. Both are the vocabulary in which modern inference engines are described.

1. Problem and motivation¶

HM(X)¶

The problem. Algorithm W interleaves traversing the program and solving equations. That makes the order of traversal part of the semantics (it decides which error you see, Lesson 7.9) and makes every extension a new algorithm: type classes need "this type must be an instance of Eq", subtyping needs "this type must be a subtype of that one", records need "this type has a field x". Odersky, Sulzmann and Wehr [OSW99] defined HM(X): the typing rules of HM, but with every judgment carrying a constraint \(C\) from an arbitrary constraint system X, and type schemes of the form \(\forall \vec\alpha.\ C \Rightarrow \tau\). They proved soundness for every X, and principal types whenever X has principal (most general) solutions. Pottier and Rémy [PR05] made the algorithmic side explicit: generate one constraint for the whole program (with special let constraints so that schemes are not re-solved at every use), then solve it with rewriting rules — Lesson 7.1's Martelli–Montanari rules plus rules for X.

OutsideIn(X)¶

The problem. A GADT pattern match brings a local fact into scope: inside case t of IsZero _ -> …, the type index a equals Bool. Constraints now have the form "if \(a \sim \mathsf{Bool}\) then …" — implications — and with them programs lose principal types: test (IsZero t) = True could have type Term a -> Bool or Term a -> a, neither more general than the other. Earlier GHC versions guessed; Vytiniotis, Peyton Jones, Schrijvers and Sulzmann [VPJSS11] designed OutsideIn(X), GHC's inference algorithm since 7.0: solve the constraints outside an implication first, never unify an outer unification variable from inside an implication whose assumptions mention it (it is untouchable there), and report an error instead of guessing. They showed that it is sound, that it never commits to a non-principal choice, and that it requires that local lets not be generalized (their companion paper "Let should not be generalised" [VPJS10]).

2. Definitions and algorithms¶

HM(X)¶

Definition 7.4.1 (Constraint system X)

A constraint system X provides predicates \(\pi(\tau_1, \dots, \tau_k)\) over types and an entailment relation \(C \Vdash D\) between constraints, where constraints are \(C ::= \mathsf{true} \mid \mathsf{false} \mid \tau_1 = \tau_2 \mid \pi(\vec\tau) \mid C_1 \wedge C_2 \mid \exists \alpha.\ C\). Entailment must be reflexive and transitive, closed under substitution (\(C \Vdash D\) implies \(\theta C \Vdash \theta D\)), and include equality reasoning (equality is a congruence). A solution of \(C\) is a substitution \(\theta\) with \(\mathsf{true} \Vdash \theta C\). Examples: \(\mathrm{X} = \{=\}\) gives HM; \(\mathrm{X} = \{=, \mathrm{Eq}\}\) with instance rules gives type classes (Lesson 7.7); \(\mathrm{X} = \{=, \mathrm{Num}\}\) with \(\mathrm{Num}(\mathsf{int})\) and \(\mathrm{Num}(\mathsf{float})\) gives Pebble's literals (Lesson 7.6).

Definition 7.4.2 (Constrained schemes and the HM(X) judgment)

A constrained type scheme is \(\forall \vec\alpha.\ C \Rightarrow \tau\). The judgment \(C, \Gamma \vdash e : \tau\) reads "under the assumption \(C\), \(e\) has type \(\tau\)". The rules are HM's (Definition 7.2.4) with \(C\) threaded through, plus (Inst) if \(\Gamma(x) = \forall\vec\alpha.\ D \Rightarrow \tau\) and \(C \Vdash [\vec\alpha \mapsto \vec\tau]D\), then \(C, \Gamma \vdash x : [\vec\alpha \mapsto \vec\tau]\tau\); (Gen) if \(C \wedge D, \Gamma \vdash e : \tau\) and \(\vec\alpha \cap \mathrm{ftv}(C, \Gamma) = \emptyset\), then \(C \wedge \exists\vec\alpha.\,D, \Gamma \vdash e : \forall\vec\alpha.\ D \Rightarrow \tau\); (Sub) if \(C, \Gamma \vdash e : \tau\) and \(C' \Vdash C\) then \(C', \Gamma \vdash e : \tau\).

Definition 7.4.3 (Constraint generation)

\(\llbracket \Gamma \vdash e : \tau \rrbracket\) is the constraint whose solutions are exactly the substitutions that type \(e\) at \(\tau\) ([PR05, §10.4]); the equation-and-predicate lists below are its conjuncts. For let it produces a let constraint: the bound expression's constraint is solved and simplified once, to a scheme, and each use instantiates the simplified scheme.

Algorithm 7.4.4 (Generate, then solve)

Input: a context \(\Gamma\) (with constrained schemes) and an expression \(e\); the rules of X for simplifying predicates.
Output: a principal constrained type \(C \Rightarrow \tau\) for \(e\), or failure with the unsatisfiable part of the constraint.
Precondition: X has principal solutions: every satisfiable constraint has a most general solution plus a residual constraint in solved form.
Postcondition: \(C, \Gamma \vdash e : \tau\) and every typing of \(e\) is an instance of \(\forall\vec\alpha.\ C \Rightarrow \tau\) (Theorem 7.4.9).
Invariant: generation does no solving (except at let); solving preserves the solution set of the constraint (each rewrite is an equivalence under X's entailment).

function Gen(Γ, e, τ):                        # returns a list of constraints
    case e of
        n:                  return [τ = int]
        x:                  ∀ᾱ. D ⇒ τx ← Γ(x);  β̄ fresh
                            return [β̄/ᾱ]D ++ [τ = [β̄/ᾱ]τx]           # Inst
        fun x -> e1:        α1, α2 fresh
                            return [τ = α1 → α2] ++ Gen(Γ[x ↦ α1], e1, α2)
        e1 e2:              α fresh
                            return Gen(Γ, e1, α → τ) ++ Gen(Γ, e2, α)
        let x = e1 in e2:   α fresh;  C1 ← Gen(Γ, e1, α)
                            (θ, D) ← Solve(C1)                        # once per let
                            σ ← ∀(ftv(θα, D) \ ftv(θΓ)). D ⇒ θα         # Gen rule
                            return equations of θ on ftv(Γ) ++ Gen(θΓ[x ↦ σ], e2, τ)
        (other forms: one equation per rule of Definition 7.2.4, as in Algorithm 7.2.9)

function Solve(C):                            # returns (θ, residual predicates)
    θ ← MGU of the equations of C             # Martelli–Montanari, Algorithm 7.1.8
    P ← θ(predicates of C)
    repeat until no rule applies:
        apply one X-rule to P:                 # e.g. Eq (τ list) ⤳ Eq τ;  Num int ⤳ true
                                               #      Num bool ⤳ false (fail)
    return (θ, P)

OutsideIn(X)¶

Definition 7.4.5 (Implication constraints; givens, wanteds; touchable variables)

Wanted constraints are \(W ::= Q \mid W_1 \wedge W_2 \mid \forall \vec a.\ (Q_g \supset W)\) where \(Q\) are simple constraints of X, \(\vec a\) are skolems (rigid type variables bound by a signature or a GADT constructor) and \(Q_g\) is the given constraint available inside (for a GADT match, the constructor's equalities). Every unification variable and every implication has a level (Lesson 7.3); a unification variable \(\alpha\) is touchable inside an implication at level \(\ell\) only if \(\mathrm{lvl}(\alpha) = \ell\). An untouchable variable may not be unified from inside the implication, because the givens could make several different solutions valid.

Algorithm 7.4.6 (OutsideIn solver, simplified)

Input: a wanted constraint \(W\) at level \(\ell\), givens \(Q_g\) (initially none).
Output: a substitution for the touchable variables and a residual \(W'\) (empty on success).
Precondition: X's simple solver \(\mathrm{simp}(Q_g, Q) = (\theta, Q')\) solves simple wanteds under givens, touching only variables of level \(\ell\).
Postcondition: every committed binding is forced (no guessing); if \(W'\) is non-empty the program is rejected or, at a top-level binding, \(W'\) is quantified (Theorem 7.4.11).
Invariant: a unification variable is assigned only at its own level; givens are used only inside their implication.

function Solve(ℓ, Qg, W):
    Qs ← simple conjuncts of W;  Is ← implications of W
    (θ, Qs') ← simp(Qg, Qs)                     # solve the simple part first ("outside")
    residual ← Qs'
    for each implication ∀ā.(Qi ⊃ Wi) in Is, at level ℓ+1:
        (θi, Ri) ← Solve(ℓ+1, Qg ∧ θQi, θWi)    # "in": givens available
        θ ← θi|level ℓ-and-deeper ∘ θ           # θi may only bind level-(ℓ+1) variables
        float out of Ri the equalities that mention no skolem of ā
            and no untouchable variable's assumption  →  append to Qs, re-run simp
        residual ← residual ∧ ∀ā.(Qi ⊃ Ri')
    return (θ, residual)

3. Worked examples¶

HM(X)¶

X = {=, Num}: Pebble's literals. For fn main() -> int { let y = 1.5; let z = y * 2; let n = 3; let m = n + 1; let s: float = m; return 0; }, generation (the oracle pebble_infer.constraints) gives one variable per integer literal (\(\nu_1\) for 2, \(\nu_2\) for 3, \(\nu_3\) for 1, \(\nu_4\) for 0) and

#	constraint	from
1	\(\mathsf{float} = \nu_1\)	`y * 2`: the operand types are equal
2	\(\nu_2 = \nu_3\)	`n + 1` (`n` has \(\nu_2\), the type of its initializer)
3	\(\nu_2 = \mathsf{float}\)	`let s: float = m` (`m` has the type of `n + 1`, i.e. \(\nu_2\))
4	\(\nu_4 = \mathsf{int}\)	`return 0`
5–10	\(\mathrm{Num}(\nu_1)\), \(\mathrm{Num}(\mathsf{float})\), \(\mathrm{Num}(\nu_2)\), \(\mathrm{Num}(\nu_3)\), \(\mathrm{Num}(\nu_2)\), \(\mathrm{Num}(\nu_4)\)	literals and the operands of `*`, `+`

Solving (Martelli–Montanari, oracle trace): eliminate \(\nu_1 := \mathsf{float}\); eliminate \(\nu_2 := \nu_3\); eliminate \(\nu_3 := \mathsf{float}\) (constraint 3 after substitution); eliminate \(\nu_4 := \mathsf{int}\). Then X's rules: \(\mathrm{Num}(\mathsf{float})\) and \(\mathrm{Num}(\mathsf{int})\) reduce to \(\mathsf{true}\); nothing is left to default. So 2, 3 and 1 are floats — including n, decided by the annotation on s three statements later. The C++ checker reaches the same types by unifying eagerly (Lesson 7.6), and tests/ch07/update_goldens.py compares the two on every golden file.

X = {=, Eq}: overloading. For fun x -> fun y -> eq x y with \(\mathit{eq} : \forall\alpha.\ \mathrm{Eq}\,\alpha \Rightarrow \alpha \to \alpha \to \mathsf{bool}\), generation instantiates \(\alpha\) to \(\beta\) and produces \(\mathrm{Eq}\,\beta\) plus the equations \(\tau = \gamma_x \to \gamma_y \to \delta\), \(\beta \to \beta \to \mathsf{bool} = \gamma_x \to \gamma_y \to \delta\); solving gives \(\gamma_x = \gamma_y = \beta\), \(\delta = \mathsf{bool}\), residual \(\mathrm{Eq}\,\beta\), and generalization gives \(\forall\beta.\ \mathrm{Eq}\,\beta \Rightarrow \beta \to \beta \to \mathsf{bool}\) — the lab corpus's corpus-classes/01-eq-fun.mml golden, Eq 'a => 'a -> 'a -> bool.

OutsideIn(X)¶

For test (IsZero t) = True with IsZero :: Term Int -> Term Bool and no signature, the generated constraint is (with \(\alpha\) the scrutinee's index and \(\rho\) the result type, both unification variables at level 1):

level	constraint	status
1	\(\mathit{Term}\ \alpha = \text{type of the argument}\)	solved: argument \(:= \mathit{Term}\ \alpha\)
2	\(\forall.\ (\alpha \sim \mathsf{Bool}) \supset (\rho \sim \mathsf{Bool})\)	\(\rho\) has level 1: untouchable at level 2
—	residual: the implication; \(\rho\) cannot be quantified (it is determined by the body)	error: "Could not deduce (\(p \sim \mathsf{Bool}\)) from the context \(a \sim \mathsf{Bool}\)"

With the signature test :: Term a -> Bool, \(\rho\) is not a unification variable at all (\(\rho = \mathsf{Bool}\) from the signature), the wanted becomes \((a \sim \mathsf{Bool}) \supset (\mathsf{Bool} \sim \mathsf{Bool})\), and it is solved trivially. eval :: Term a -> a has wanted \((a \sim \mathsf{Int}) \supset (a \sim \mathsf{Int})\) in its first equation, discharged by the given. GHC's messages for both are in §7.

4. Invariants and correctness¶

HM(X)¶

Theorem 7.4.7 (HM(X) is sound for every X)

If \(C, \Gamma \vdash e : \tau\) and \(\theta\) is a solution of \(C\) (and of the constraints of \(\Gamma\)), then \(e\) does not go wrong under the semantics of X's predicates; in particular for X = {=} this is HM's soundness.

Proof sketch (full proof: [OSW99, §4]; for the constraint-based presentation [PR05, §10.5])

The semantic proof of Milner [Mil78] carries over: interpret a constrained scheme \(\forall\vec\alpha.\,D \Rightarrow \tau\) as the intersection of the meanings of its instances whose constraint holds. Rule by rule, the only new cases are Inst — which is sound because \(C \Vdash [\vec\tau/\vec\alpha]D\) transports the solution — and Gen, whose side condition keeps the quantified variables independent of \(C\) and \(\Gamma\). Nothing depends on what the predicates are, only on the properties of entailment in Definition 7.4.1.

Theorem 7.4.8 (Constraint generation is exact)

For every \(\Gamma\), \(e\), \(\tau\): \(\theta\) solves \(\llbracket\Gamma \vdash e : \tau\rrbracket\) iff \(\theta\Gamma \vdash e : \theta\tau\) in HM(X) (with \(\theta\) making the constraints of \(\Gamma\) true).

Proof sketch (full proof: [PR05, §10.4])

By induction on \(e\), one case per construct, using that each generated conjunct is exactly the premise of the corresponding rule of Definition 7.2.4 read as an equation on fresh variables, and that the existential quantification of fresh variables in the let-constraint corresponds to the choice of instance in Inst. The let case uses the lemma that solving a let-constraint's right-hand side once and instantiating the simplified scheme is equivalent to instantiating the unsolved constraint at every use (the solution sets coincide because simplification preserves solutions).

Theorem 7.4.9 (Principal types in HM(X))

If X has principal solutions (every satisfiable constraint \(C\) has a solution \(\theta\) and residual \(D\) such that the solutions of \(C\) are exactly the instances of \(\theta\) satisfying \(D\)), then every typable \(e\) has a principal constrained type, and Algorithm 7.4.4 computes it.

Proof sketch (full proof: [OSW99, §5])

Combine Theorem 7.4.8 with the principal-solution property: the solutions of \(\llbracket\Gamma \vdash e : \alpha\rrbracket\) are the instances of \((\theta, D)\), so \(\forall\vec\alpha.\,D \Rightarrow \theta\alpha\) has every typing of \(e\) as an instance, by the Sub and Inst rules. For X = {=}, the principal solution is the MGU and \(D = \mathsf{true}\) (Lesson 7.1): Theorem 7.2.11 is the special case. For X = Num (Pebble), the residual \(\mathrm{Num}(\nu)\) on an unconstrained variable has two incomparable solutions; Pebble defaults it to int (Lesson 7.6) — a choice HM(X) itself does not make.

OutsideIn(X)¶

Proposition 7.4.10 (GADT matches lose principal types)

test (IsZero t) = True, with data Term a where IsZero :: Term Int -> Term Bool (and a constructor Lit :: Int -> Term Int), has both types Term a -> Bool and Term a -> a, and no type of which both are instances.

Proof

Term a -> Bool: the body True has type Bool everywhere. Term a -> a: inside the match, the given \(a \sim \mathsf{Bool}\) holds, so True : Bool also has type a. No common generalization: a type more general than both would be Term a -> r with r a variable independent of a (instances r := Bool and r := a), i.e. test : ∀a r. Term a -> r; but then test (IsZero (Lit 0)) :: Int would be derivable, while the body produces True — unsound. Any other candidate must fix the result to Bool or to a, and then the other type is not an instance.

Theorem 7.4.11 (OutsideIn(X) is sound and never guesses)

If OutsideIn(X) accepts a program with a type, the program is well typed in the declarative system with local assumptions; every unification it performs is forced by the constraints (it holds in every solution), so it never commits to one of several incomparable types; with MonoLocalBinds (no generalization of local lets without signatures) the accepted programs have principal types among the typings the algorithm considers.

Proof sketch (full proof: [VPJSS11, §5–6]; the need for MonoLocalBinds: [VPJS10])

Soundness by induction on the solver's steps, each justified by the simple solver's soundness for X and by the rule that an implication's givens are used only inside it. No guessing: a unification variable is assigned only at its own level (touchability), where all constraints mentioning it are in scope; an untouchable variable inside an implication could be assigned differently under different givens (Proposition 7.4.10 is the witness), so the solver leaves it and reports it. The principality statement needs local lets to be monomorphic because generalizing a local let over a variable that later receives a given makes the let's scheme depend on facts outside it.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
HM(X), X = equality	as HM: DEXPTIME-complete; near-linear in practice	near-linear	constraints \(O(n)\) before solving	\(n\) program size
HM(X), X = type classes	as HM plus instance resolution per predicate; undecidable with unrestricted instances (GHC's `UndecidableInstances`, bounded by `-freduction-depth`)	linear in the number of predicates	residual constraints can double per `let` (below)	\(p\) predicates
OutsideIn(X)	as HM(X) for its X, plus one solver pass per implication, repeated when equalities float out	near-linear on ordinary code; GADT-heavy code dominated by type-family reduction	the implication tree mirrors the program's match nesting	\(i\) implications

Justification. Generation emits \(O(1)\) conjuncts per construct, so \(O(n)\) constraints; solving the equalities is Algorithm 7.1.10; each predicate simplification step is one instance-rule application; implications add at most one re-solve per floated equality, and each float reduces the number of unsolved equalities.

Pathological family (constraint doubling). With NoMonomorphismRestriction, x0 z = z == z, x1 = (x0, x0), x2 = (x1, x1), …: \(x_i\)'s scheme has \(2^i\) independent type variables, each with its own Eq predicate, because both copies of \(x_{i-1}\) are instantiated independently — the pair tower of Lesson 7.3 with a predicate on every leaf. At run time, each is a dictionary parameter (Lesson 7.7). GHC's real output for \(x_2\) is in §7: four Eq constraints.

HM(X)¶

Qualified types (Jones [Jon94]): HM with predicates, the theory behind Haskell's type classes; predicates in schemes, entailment by instances, and evidence (dictionaries) as a translation. Trade-off: one particular X, worked out with its compilation.
HM(Sub) and structural subtyping with constraints [OSW99]: X = subtyping inequalities; principal types exist but grow, so constraint simplification becomes the engineering problem. Trade-off: expressive (records, objects), costly types.
Let-constraints with early simplification [PR05]: simplify the constraint of a let before generalizing, so that schemes stay small. Trade-off: essential for near-linear performance; the simplifier must preserve solutions exactly.

OutsideIn(X)¶

MonoLocalBinds [VPJS10]: do not generalize local bindings without signatures (on by default with GADTs or type families). Trade-off: loses some local polymorphism, gains principal types and a simpler solver.
Bidirectional GADT checking (GHC in practice, and Lesson 6.4's modes): require a signature for functions that match on GADTs, so the result type is known inside implications. Trade-off: an annotation per GADT function; no untouchable-variable errors.
Quick Look for impredicativity (Lesson 7.8, [SHPJV20]): an extra inference step before OutsideIn's solver for arguments of polymorphic type. Trade-off: local, predictable, and incomplete by design.

7. In real compilers¶

HM(X)¶

GHC generates constraints with evidence placeholders during type checking and solves them afterwards: simplifyInfer in compiler/GHC/Tc/Solver.hs simplifies the constraints of a binding and decides what to quantify over [GHC-Solver]; class constraints are solved by matchGlobalInst in compiler/GHC/Tc/Instance/Class.hs [GHC-Class]. Swift generates a constraint system per expression and solves it by search (Lesson 7.5). LLVM TableGen infers the types of instruction-selection patterns by constraint propagation to a fixed point: TreePattern::InferAllTypes in llvm/utils/TableGen/Common/CodeGenDAGPatterns.cpp repeatedly calls ApplyTypeConstraints on every pattern tree until nothing changes, narrowing sets of possible machine value types instead of unifying single types [TBLGEN-Patterns].

Inferred constrained schemes in GHC 9.4, including the doubling family

Reproduce (GHC 9.4.7):

mkdir -p hs && cat > hs/Constraints.hs <<'EOF'
{-# LANGUAGE NoMonomorphismRestriction #-}
module Constraints where
member x []     = False
member x (y:ys) = x == y || member x ys
between lo hi x = lo <= x && x <= hi
x0 z = z == z
x1 = (x0, x0)
x2 = (x1, x1)
EOF
LC_ALL=C ghc -fno-code -ddump-types hs/Constraints.hs

Output (the [1 of 1] Compiling line removed):

TYPE SIGNATURES
  between :: forall {a}. Ord a => a -> a -> a -> Bool
  member :: forall {t}. Eq t => t -> [t] -> Bool
  x0 :: forall {a}. Eq a => a -> Bool
  x1 :: forall {a1} {a2}. (Eq a1, Eq a2) => (a1 -> Bool, a2 -> Bool)
  x2 ::
    forall {a1} {a2} {a3} {a4}.
    (Eq a1, Eq a2, Eq a3, Eq a4) =>
    ((a1 -> Bool, a2 -> Bool), (a3 -> Bool, a4 -> Bool))
Dependent modules: []
Dependent packages: [base-4.17.2.0]

What to notice: every scheme is \(\forall\vec\alpha.\ C \Rightarrow \tau\) (Definition 7.4.2). between uses both <= (Ord) and nothing else, and Ord a entails Eq a by the superclass, so the simplifier keeps only Ord a — X's entailment at work. x1 and x2 are the §5 family: the predicates double with the pairs.

OutsideIn(X)¶

GHC is the implementation: implications are the Implication records of compiler/GHC/Tc/Types/Constraint.hs (with their level ic_tclvl and givens ic_given), solved by solveImplication and solveWanteds in compiler/GHC/Tc/Solver.hs; touchability is isTouchableMetaTyVar in compiler/GHC/Tc/Utils/TcType.hs [GHC-Solver, GHC-TcType].

An untouchable result type in GHC 9.4

Reproduce (GHC 9.4.7):

mkdir -p hs && cat > hs/Gadt.hs <<'EOF'
{-# LANGUAGE GADTs #-}
module Gadt where

data Term a where
  Lit    :: Int  -> Term Int
  IsZero :: Term Int -> Term Bool

eval :: Term a -> a
eval (Lit n)    = n
eval (IsZero t) = eval t == 0

test (IsZero t) = True
EOF
LC_ALL=C ghc -fno-code hs/Gadt.hs

Output (the [1 of 1] Compiling line removed):

hs/Gadt.hs:12:19: error:
    * Could not deduce (p ~ Bool)
      from the context: a ~ Bool
        bound by a pattern with constructor:
                   IsZero :: Term Int -> Term Bool,
                 in an equation for `test'
        at hs/Gadt.hs:12:7-14
      `p' is a rigid type variable bound by
        the inferred type of test :: Term a -> p
        at hs/Gadt.hs:12:1-22
    * In the expression: True
      In an equation for `test': test (IsZero t) = True
    * Relevant bindings include
        test :: Term a -> p (bound at hs/Gadt.hs:12:1)
    Suggested fix: Consider giving `test' a type signature
   |
12 | test (IsZero t) = True
   |                   ^^^^

What to notice: eval, with its signature, is accepted: inside each equation the given (\(a \sim \mathsf{Int}\) or \(a \sim \mathsf{Bool}\)) discharges the wanted. test has none: the wanted \(p \sim \mathsf{Bool}\) lives inside the implication "from the context: a ~ Bool", and \(p\) belongs to the outer level, so the solver may not choose \(p := \mathsf{Bool}\) there (Proposition 7.4.10 shows \(p := a\) would be just as valid). GHC reports the stuck implication and suggests the signature — §3's table.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
HM(X)	Sound for every X (Theorem 7.4.7); principal types when X has principal solutions (Theorem 7.4.9)	As HM plus X's solver; near-linear for equality and simple classes	The unsolved residual constraint is the error; order-independent (Lesson 7.9)	Medium: a generator, a solver, X's rules; proofs reused	GHC's constraint generation, the Pebble oracle, Swift's per-expression systems, research extensions
OutsideIn(X)	GADTs and type families with local assumptions; sound and guess-free (Theorem 7.4.11); principal only with MonoLocalBinds	As HM(X) plus implication passes · fine in practice	"Could not deduce … from the context …" and untouchable-variable errors; suggests signatures	High: levels, implications, floating, evidence	GHC since 7.0

Choose HM(X) as the architecture of any inference engine that will grow: it keeps the traversal independent of the solving, gives order-independent error reports, and lets the constraint language grow without new proofs. Choose OutsideIn(X) when the type system has local assumptions (GADTs, type families, existential packs); otherwise its extra machinery costs you error messages about untouchable variables for nothing.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
HM(X)	`hmx-residual`, `hmx-pebble-solution`, `find-tablegen-inference`	— (constraint generation and solving are traced by the `unification` drill for equalities; the Pebble instance by the lab goldens and the quiz)	`hm-x`	E1–E2 (Pebble's constraints)
OutsideIn(X)	`outsidein-untouchable`, `gadt-principal`	— (GADT inference has no small randomized generator that stays meaningful; the quiz traces the implication of §3)	`outsidein`	—

References¶

See the chapter references.

Lesson 7.4 — Constraint-based inference: HM(X) and OutsideIn(X)¶

1. Problem and motivation¶

HM(X)¶

OutsideIn(X)¶

2. Definitions and algorithms¶

HM(X)¶

OutsideIn(X)¶

3. Worked examples¶

HM(X)¶

OutsideIn(X)¶

4. Invariants and correctness¶

HM(X)¶

OutsideIn(X)¶

5. Complexity¶

6. Variants and refinements¶

HM(X)¶

OutsideIn(X)¶

7. In real compilers¶

HM(X)¶

OutsideIn(X)¶

8. Comparison¶

9. Assessment¶

References¶