Chapter 7 · Type Inference¶

Part 1 · Front End · about 3 weeks · Previous: Ch 6 · Next: Ch 8

The problem¶

Chapter 6's checkers verify types that are written down or pushed in from context. Type inference computes the types nobody wrote: the type of fun f -> fun x -> f (f x), the element type of Vec::new() from a push three lines later, the type of the literal 2 in y * 2. The input is a program with missing annotations (in ML, all of them; in Rust, Kotlin, TypeScript and Pebble, those inside bodies); the output is a type for every expression and declaration — the most general one, when the type system guarantees one exists — or an error that says which constraints could not all hold. Every technique in this chapter reduces the problem to constraints between types with unknowns and solves them: by unification (Robinson, Martelli–Montanari, union-find), by Hindley–Milner's generalization and instantiation (Algorithms W, J and M, levels, the value restriction), by constraint solving with type classes and local assumptions (HM(X), OutsideIn(X)), by search over overloads (Swift), and within the local scopes that Rust, Kotlin, TypeScript and Pebble choose. In pebblec's world this is inferTypes (pebble/include/pebble/Sema/Infer.h, pebble-spec §8.9), Chapter 6's checker rebuilt on unification.

What you will be able to do¶

Compute most general unifiers by hand with Robinson's, Martelli–Montanari's and the union-find algorithm, and explain why each terminates and when the occurs check fires.
Trace Algorithms W, J and M on a program, give the principal type of every subterm, and predict where each reports an error.
Decide generalization at every let with levels and the value restriction, and construct programs whose types grow exponentially.
Explain HM(X) and OutsideIn(X): what a constraint system provides, why GADT matches create implications, and what "untouchable" means.
Explain why Swift's type checker can take exponential time, build the reduction from 3-SAT, and name its mitigations.
Compare the inference scopes of Rust, Kotlin, TypeScript and Pebble on concrete programs, and implement inferTypes (./course test 7).
Resolve type-class constraints to dictionaries, check coherence, and translate a program to dictionary passing or predict its monomorphized instances.
Localize type errors by traversal order, minimal unsatisfiable subsets and provenance, and find each technique in OCaml, GHC, rustc, Swift, tsc, Kotlin and LLVM sources.

Prerequisites: Ch 6 (judgments, bidirectional checking with its literal rule, Lesson 6.9's implementation of generics) and Ch 5 (resolved names). Proofs are by induction on terms and derivations, as in Chapter 6.

Notation¶

Shared notation follows the house notation (§1 sets and functions, §6 types and semantics, §8 complexity). In this chapter \(\alpha, \beta, \gamma\) are type variables (not grammar strings), and:

Symbol	Meaning
\(f(t_1, \dots, t_n)\), \(x, y, z\), \(\mathrm{vars}(t)\), \(\lvert t \rvert\)	first-order terms, variables, the variables of a term, its size (Definition 7.1.1)
\(\theta = [x \mapsto t]\), \(\theta_2\theta_1\), \(\theta \preceq \theta'\)	a substitution, composition (apply \(\theta_1\) first), "more general than" (Definitions 7.1.2–7.1.3)
\(s \doteq t\), \(U(E)\), MGU	an equation to unify, the unifiers of \(E\), a most general unifier (Definition 7.1.3)
\(\mathrm{find}\), \(\mathrm{union}\), \(\alpha(n)\)	union-find operations; the inverse Ackermann function (Lesson 7.1 §5)
\(\forall\vec\alpha.\,\tau\), \(\tau \le \sigma\), \(\mathrm{ftv}\), \(\mathrm{gen}(\Gamma, \tau)\)	type schemes, instances, free type variables, generalization (Definitions 7.2.1–7.2.2)
\(\mathrm{lvl}(\alpha)\), \(\ell\), \(\mathsf{generic}\)	the level of a type variable, the current level, the level of quantified variables (Definition 7.3.1)
\(C, \Gamma \vdash e : \tau\), \(\forall\vec\alpha.\,C \Rightarrow \tau\), \(C \Vdash D\)	HM(X) judgments, constrained schemes, entailment (Definitions 7.4.1–7.4.2)
\(\forall\vec a.\,(Q_g \supset W)\)	an implication constraint with givens \(Q_g\) and wanteds \(W\) (Definition 7.4.5)
\(T_i\), \(c_1 \vee \dots \vee c_k\)	Swift-style type variables and disjunctions (Definition 7.5.1)
\(\nu\), \(K(\nu)\), \(d(\nu)\)	a literal (numeric) type variable, its allowed types, its default (Definition 7.6.2)
\(C\ \tau\), \(D_C\)	a class predicate; the dictionary (evidence) type of class \(C\) (Definitions 7.7.1–7.7.2)
\(\sigma_1 \le \sigma_2\) (polymorphic), rank	subsumption between polymorphic types; the rank of a type (Definitions 7.8.1–7.8.2)
\((\ell, c)\), MUS	a labelled constraint, a minimal unsatisfiable subset (Definitions 7.9.1–7.9.2)

Technique map¶

Family	Techniques (origin)	Lesson
Unification	Robinson's algorithm (Robinson 1965); the Martelli–Montanari rule system (1982); union-find unification (Huet 1976; linear: Paterson & Wegman 1978); the occurs check and rational trees	7.1
Hindley–Milner	let-polymorphism and principal types (Hindley 1969; Milner 1978; Damas & Milner 1982); Algorithm W (Milner 1978); Algorithm J (Milner 1978); Algorithm M (Lee & Yi 1998)	7.2
HM in practice	level-based generalization (Rémy 1992; OCaml); the value restriction (Wright 1995, after Tofte 1990; relaxed: Garrigue 2004); complexity: DEXPTIME-complete (Mairson 1990; Kfoury, Tiuryn & Urzyczyn 1990), near-linear in practice (McAllester 2003)	7.3
Constraint-based inference	HM(X) (Odersky, Sulzmann & Wehr 1999; Pottier & Rémy 2005); OutsideIn(X) (Vytiniotis, Peyton Jones, Schrijvers & Sulzmann 2011)	7.4
Search-based inference	Swift's constraint solver: disjunctions, components, scoring, and its exponential cases (the Swift type checker, `docs/TypeChecker.md`)	7.5
Local and flow-based inference	Rust (body-local unification, literal fallback); Kotlin (declaration-local, builder inference); TypeScript (widening, contextual and flow types); Pebble's inference mode (pebble-spec §8.9)	7.6
Type classes and traits	instance resolution (Wadler & Blott 1989; Jones 1994); coherence (Haskell 98, Rust RFC 1023/2451); dictionary passing vs monomorphization (Hall, Hammond, Peyton Jones & Wadler 1996; rustc)	7.7
Beyond rank 1 (overview)	higher-rank polymorphism (Odersky & Läufer 1996; Peyton Jones et al. 2007; Dunfield & Krishnaswami 2013); impredicativity and Quick Look (Serrano et al. 2020); undecidability of System F inference (Wells 1999)	7.8
Error localization	blame by traversal order (W, J, M; McAdam 1998); minimal unsatisfiable subsets and minimum error sources (Haack & Wells 2004; Pavlinovic, King & Wies 2014; Zhang & Myers 2014); provenance notes	7.9

flowchart LR
  subgraph UNI[Unification]
    ROB[Robinson 1965] -->|rules, not a loop| MM[Martelli-Montanari 1982]
    MM -->|share terms| UF[Union-find<br/>Huet 1976]
    OC[Occurs check] --- UF
  end
  subgraph HM[Hindley-Milner]
    LP[let-polymorphism<br/>DM 1982] --> W[Algorithm W]
    W -->|in-place| J[Algorithm J]
    W -->|expected type| M[Algorithm M<br/>Lee-Yi 1998]
  end
  subgraph PRAC[HM in practice]
    LV[Levels<br/>Remy 1992] --- VR[Value restriction<br/>Wright 1995]
    CX[DEXPTIME / near-linear]
  end
  subgraph CON[Constraint-based]
    HMX[HM X<br/>1999] -->|local assumptions| OI[OutsideIn X<br/>GHC 2011]
    SW[Swift solver<br/>disjunctions + search]
  end
  subgraph LOC[Local inference]
    RS[Rust] --- KT[Kotlin] --- TS[TypeScript] --- PB[Pebble 8.9]
  end
  subgraph TC[Type classes]
    IR[Instance resolution<br/>WB 1989] --> COH[Coherence] --> DP[Dictionaries vs<br/>monomorphization]
  end
  subgraph BEY[Beyond rank 1]
    HR[Higher rank] --> IMP[Impredicativity<br/>Quick Look]
  end
  subgraph ERR[Error localization]
    TB[Traversal blame] --- MUS[MUS / min error source] --- PROV[Provenance]
  end
  UF --> J
  J --> LV
  W --> HMX
  HMX --> IR
  HMX --> SW
  UF --> PB
  M --> TB
  HMX --> MUS
  OI --> HR

Who uses what¶

System	Technique	Notes
OCaml 4.14	Algorithm J with levels (`ctype.ml`), expected types in `type_expect`, the relaxed value restriction, `-rectypes` rational trees	Lessons 7.1–7.3, 7.9
GHC 9.4	OutsideIn(X) with implications and `TcLevel`; type classes with dictionary passing and `SPECIALIZE`; `RankNTypes`, Quick Look	Lessons 7.4, 7.7, 7.8
SML/NJ 110	W-style blame; SML '97 value restriction	Lessons 7.2, 7.3
rustc 1.94	body-local unification in `ena` tables, `{integer}` fallback to `i32`, trait selection, coherence (orphan and overlap), monomorphization	Lessons 7.1, 7.6, 7.7
Swift 6.3	per-expression constraint solving with disjunctions, component splitting, favoring and limits	Lesson 7.5
Kotlin 2.2	declaration-local inference, builder inference (PCLA)	Lesson 7.6
tsc 6.0	widening, best common type, contextual typing, evolving arrays, flow types	Lesson 7.6
Clang/LLVM 23	template argument deduction as one-sided unification (`SemaTemplateDeduction.cpp`), `auto`; union-find in `EquivalenceClasses`; TableGen's pattern type inference	Lessons 7.1, 7.4, 7.6
`pebblec`	Chapter 6's `typeCheck`; the Chapter 7 checker `inferTypes` (numeric variables, defaulting, E0416) in `ch07-infer`	Exercises

Comparison¶

Every row is the corresponding lesson's §8 row.

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Robinson's algorithm	Computes an MGU or proves none exists (Theorem 7.1.14)	Exponential on \(E_n\) with trees · fine for small types	Reports the first disagreement pair: two concrete subterms	Lowest: one loop, one substitution	Textbooks, theorem provers, one-sided template deduction (Clang)
Martelli–Montanari	Same solutions, with a proof that separates rules from strategy (Theorem 7.1.15); extends to E-unification and constraint stores	Exponential with trees; efficient with multi-equations [MM82] · rule-at-a-time	The failing rule and equation, and the history of rewrites that produced it	Low for the rules; strategy and data structures chosen separately	Specifications, GHC's canonicalizer, constraint solvers
Union-find unification	Same solutions (Theorem 7.1.17), on shared graphs	\(O(N\,\alpha(N) k)\) · near-linear; the §5 family in linear time	Failures found on classes; messages must re-read the terms	Medium: union-find, schemas, read-back, cycle check	OCaml, GHC, rustc (`ena`), Swift, Pebble's `inferTypes` (E2)
The occurs check	Excludes exactly the cyclic solutions (Lemma 7.1.18)	Eager: \(O(N^2)\) total; deferred: \(O(N)\)	Eager: at the offending binding; deferred: needs reconstruction	Low	Every type checker for finite types; omitted by Prolog; relaxed by `-rectypes`
Let-polymorphism (HM)	Principal types for every typable program (Theorem 7.2.11); rank-1 only, λ-bound variables monomorphic (Proposition 7.2.10)	DEXPTIME-complete · near-linear in practice (Lesson 7.3)	Types need no annotations; errors can be far from the mistake	The rules are small; generalization needs care	ML, OCaml, Haskell 98, F#, the lab's MiniML
Algorithm W	Sound and complete (Theorem 7.2.11)	\(\Theta(n^2)\) extra on nested lets · lab: 286 ms at \(n = 2000\)	Blames the application where two synthesized types clash	Low; purely functional	Proofs, teaching, reference implementations
Algorithm J	Same results as W (Theorem 7.2.12)	Near-linear with union-find and levels · lab: 0.87 ms at \(n = 2000\)	Same locations as W	Medium: mutable graph, dereferencing	OCaml, GHC, rustc, SML/NJ — every production HM
Algorithm M	Same types as W; fails no later (Theorem 7.2.13)	As W, one unification per leaf more · lab: 818 ms at \(n = 2000\) (substitution-based)	Blames the leaf that contradicts the expected type	Low; like bidirectional checking	OCaml's `type_expect`, GHC's expected types; error-reporting passes
Level-based generalization	Exactly \(\mathrm{gen}(\Theta\Gamma, \tau)\) (Theorem 7.3.8)	\(O(\lvert\tau_1\rvert)\) per `let` · lab: J 0.87 ms vs W 286 ms at \(n = 2000\)	Same types; `'_weak` variables are levels that were lowered	Low once union-find exists: an integer per variable, a `min` in `BindVar`	OCaml, GHC (`TcLevel`), the lab's J
The value restriction	Sound with references (Theorem 7.3.10a); rejects some pure programs (η-expansion fixes them)	\(O(\lvert e_1\rvert)\) per `let` · negligible	Weak variables; SML/NJ warns, F# errors (FS0030)	Very low: one syntactic test	SML '97, OCaml (relaxed [Gar04]), F#, the lab
Complexity of HM inference	DEXPTIME-complete (Theorem 7.3.11)	\(2^{O(n)}\) worst · near-linear for bounded let-depth and type size [McA03]	Exponential types are unreadable before they are slow	— (a property, not an implementation)	Explains generated-code and functor blow-ups; motivates shared types
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
Swift's constraint solver	Overloads, literals of many types, generics, conversions and bidirectional flow within an expression; exact best solution by score (Theorem 7.5.5)	Exponential worst case, NP-hard (Proposition 7.5.6) · microseconds typically; seconds, or the "reasonable time" error, on the §7 tests	Excellent when one solution exists; ambiguity and "too complex" errors name no culprit	Very high: generation, graph splitting, disjunction heuristics, scoring, diagnostics by "fixes"	Swift; the model in `tools/course/lib/overload.py`
Rust	Unification over a whole body; literals decided by later uses; fallback `i32`/`f64` (Proposition 7.6.8); no generalization	near-linear unification; trait selection bounded by limits	E0282 "type annotations needed" with a suggested annotation; mismatch errors name the expected type's origin	High: tables, obligations, fallback, expectations	Rust
Kotlin	Declaration-local; builder inference for lambdas (Proposition 7.6.9); literals take expected integer types	per call · fast	"cannot infer type for type parameter"; mismatches at the use	High (K2's PCLA)	Kotlin, DSLs built on builders
TypeScript	Initializer types widened (Proposition 7.6.10); contextual typing; evolving flow types	linear-ish with caches	Errors at assignments against the declared type; implicit-`any` for uninferable parameters	High: widening, flow graph, generic inference	TypeScript, and JavaScript tooling
Pebble's inference mode	Conservative extension of Chapter 6 (Theorem 7.6.11); literals and bindings decided anywhere in the body; default `int`	\(O(n\,\alpha(n))\) per function · the same as Chapter 6's checker	Chapter 6's diagnostics, plus E0416 with the first binding's origin	Low: Chapter 6's checker plus a two-point union-find	`ch07-infer`, exercises E1–E4
Instance resolution	Overloading that composes with HM; evidence per predicate (Theorem 7.7.7); undecidable with unrestricted instances	\(O(\lvert\tau\rvert)\) per predicate under H98 rules	"no instance" / E0277 with the originating bound; ambiguity errors	Medium: a small logic-program solver with evidence	Haskell, Rust, Scala, Swift, Lean
Coherence	At most one evidence per closed predicate, globally (Theorem 7.7.8)	pairwise head unification, indexed	Rust: errors at the impl (E0117, E0119); GHC: at the use site	Low for the checks; the orphan rule is a language-design decision	Rust (strict), Haskell (overlap check, orphans warned), not Scala
Dictionary passing	One copy; polymorphic recursion and separate compilation work (Theorem 7.7.9)	indirect call per method; GHC specializes hot paths	Generic code errors once, at the definition	Low: extra parameters in the translation	GHC by default, Swift witness tables, the lab's L5
Monomorphization	Fastest code; needs finitely many instantiations	code size grows with instantiations (§5)	Errors per generic definition (Rust) or per instance (C++)	Medium: a collector, symbol mangling	Rust, C++, GHC with `SPECIALIZE`
Higher-rank polymorphism	Arbitrary rank with annotations; complete and decidable for predicative instantiation (Theorem 7.8.5); no principal types without annotations (Proposition 7.8.6)	as HM · negligible overhead	Rigid/skolem-escape errors; clear once annotated	Medium: skolems, subsumption, levels	GHC `RankNTypes`, `runST`, Scala 3, OCaml record fields
Impredicativity	Polymorphic instantiation where one application forces it (Theorem 7.8.7a); full System F undecidable (Theorem 7.8.7b)	linear extra pass · negligible	Fails predictably: only local evidence is used	Medium (Quick Look) to very high (MLF)	GHC `ImpredicativeTypes`; research languages
Blame by traversal order	Reports one constraint of some MUS (Proposition 7.9.7); order-dependent	free	Often the last of several conflicting uses; M improves it	none beyond inference	every production compiler (OCaml, GHC, rustc, Swift, SML/NJ)
Minimal unsatisfiable constraint sets	All explanations; minimum error sources are order-independent (Theorem 7.9.8)	exponential worst case; seconds with MaxSMT [PKW14]	Precise slices; the most likely culprit ranked first	High: constraint generation with labels, a solver loop	Research tools (SHErrLoc, MinErrLoc), the course oracle
Provenance notes	Explains the other half of a two-location conflict (Proposition 7.9.9)	\(O(1)\) per binding	Two locations, one of them the origin; readable	Low	rustc, GHC, OCaml, Pebble's E0416

Comparison-lab results (reproduce with build/<preset>/bin/ch07-hm-bench; reference solutions, RelWithDebInfo, the course container): on letChain with \(n = 250, 500, 1000, 2000\), W takes 4.2, 13.8, 58.4, 286 ms, J 0.11, 0.20, 0.54, 0.87 ms and M 10.8, 39.1, 153, 818 ms; on nestedLets W takes 1036 ms and J 1.95 ms at \(n = 2000\); on pairTower all three are exponential (at \(n = 14\): W 672, J 470, M 742 ms for a 338 285-character type). All three agree on every corpus program's type and on 500 random programs; the ★ dictionary translation of every corpus-classes program evaluates to its expected value.

Route through this chapter¶

Step	What	Techniques	How it is exercised
1	Lesson 7.1	Robinson, Martelli–Montanari, union-find, occurs check	drill `unification`; quiz
2	Lesson 7.2 and lab L1–L3	let-polymorphism, W, J, M	drill `hm-trace`; `ch07.HM.L1_`–`L3_`
3	Lesson 7.3 and lab L2, L4	levels, value restriction, complexity	drill `generalization`; `ch07-hm-bench`
4	Lesson 7.4	HM(X), OutsideIn(X)	quiz; the Pebble oracle `pebble_infer`
5	Lesson 7.6 and Exercises E1–E4	Rust, Kotlin, TypeScript, Pebble's inference mode	`ch07.Infer.*`, `ch07.lit`
6	Lesson 7.5	Swift's solver	quiz (computed with `overload.py`)
7	Lesson 7.7 and ★ lab L5	instance resolution, coherence, dictionaries vs monomorphization	`ch07.HM.L5_*`; quiz
8	Lesson 7.8	higher rank, impredicativity	quiz; flashcards
9	Lesson 7.9	traversal blame, MUS, provenance	quiz; `hm-trace --difficulty hard`
10	Theory test	all	`./course quiz 7` (≥ 80 % to finish)

Pebble implements union-find unification with numeric variables and provenance (E0416); the comparison lab implements W, J and M (and ★ dictionary passing); Swift's solver, HM(X)/OutsideIn(X), coherence, higher rank and MUS localization are theory with computed quiz items and the Python models in tools/course/lib/ (hm.py, overload.py, pebble_infer.py).

Practice and check¶

./course drill unification --difficulty easy     # warm up; --solution shows every step
./course drill hm-trace
./course drill generalization --difficulty hard
./course flash 7                                 # daily, a few minutes
./course quiz 7                                  # after the lessons
./course test 7                                  # after the exercises and the lab
./course status                                  # done = quiz ≥ 80 % and tests pass

References¶

The chapter's annotated bibliography — papers, textbook sections, pinned source files, docs — is in references.md. Start with: [TAPL] (Ch. 22), [DM82] and [Mil78] (Hindley–Milner), [MM82] (unification as rewriting), [PR05] (constraint-based inference), [Wri95] (the value restriction), [VPJSS11] (OutsideIn(X)), [WB89] (type classes) and [SWIFT-TypeCheckerDoc] (Swift's solver).