Lesson 7.9 — Error localization in type inference¶

Techniques: blame by traversal order — report the unification that fails first, as W, J and M do; its left-to-right bias and M's earlier detection (Lee & Yi 1998 [LY98]; McAdam's analysis of W's bias [McA98]); minimal unsatisfiable constraint sets and minimum error sources — treat the program's constraints as a set, find the minimal conflicting subsets and the fewest program locations that explain all of them (Haack & Wells 2004 [HW04]; Pavlinovic, King & Wies 2014 [PKW14]; SHErrLoc, Zhang & Myers 2014 [ZM14]); provenance notes — remember why each type variable was bound and cite that origin (rustc's "expected due to this", GHC's "arising from", Pebble's E0416 note) · Pebble implements: provenance for E0416 (inferTypes, exercise E3) · Drills: — (see §9) · Prerequisites: Lessons 7.2, 7.4, 7.6 · Time: 3 hours

A type error in an inferred program is a set of constraints that cannot hold together, but a compiler reports a point. Which point? The one where the solver happened to notice (traversal order), the one that belongs to the fewest explanations (constraint-based localization), or a point plus the history that led there (provenance)? The first is free, the second costs search, the third costs bookkeeping. This lesson compares them on one small program, where all real compilers blame a location that a one-token fix elsewhere would repair.

1. Problem and motivation¶

Blame by traversal order¶

The problem. W reports the first unification that fails in its left-to-right, bottom-up order (Lesson 7.2); J the same; M the first leaf that contradicts its expected type. None of them looks at the program's other evidence. McAdam [McA98] showed that W's order makes its messages biased: the same inconsistency is blamed differently when the program's subterms are permuted, and the location is often the last of several conflicting uses rather than the odd one out. This is the default behavior of every production inference engine because it costs nothing, so a compiler writer must know its failure modes.

Minimal unsatisfiable constraint sets¶

The problem. If a program is ill typed, its constraint set (Lesson 7.4) is unsatisfiable. Haack and Wells [HW04] proposed reporting a minimal unsatisfiable subset (MUS) — a set of constraints that conflict but each of which is needed for the conflict — as a type error slice: every program location in it is implicated, none is noise. A program can have several MUSes; Pavlinovic, King and Wies [PKW14] and Zhang and Myers (SHErrLoc [ZM14]) rank locations by how many MUSes they explain: a minimum error source is a smallest set of locations that intersects every MUS — changing those locations can make the program typable. This makes the report order-independent, at the price of calling a solver many times.

Provenance notes¶

The problem. Even with traversal-order blame, a report becomes useful if it says why the conflicting type was expected: "expected u64 because of this annotation", "n was inferred as int here". The solver must record, for each binding of a type variable, the constraint (and so the program location) that caused it — cheap, local bookkeeping. rustc's "expected due to this", GHC's "arising from a use of +", OCaml's "because it is in the condition of an if-statement", and Pebble's E0416 note are all provenance.

2. Definitions and algorithms¶

Definition 7.9.1 (Labelled constraints; error slice)

A labelled constraint is a pair \((\ell, c)\) of a program location \(\ell\) and an equation \(c\) produced for the subterm at \(\ell\) (Algorithm 7.9.4). For a set \(S\) of labelled constraints, \(\mathrm{locs}(S)\) is the set of their locations. A set \(S\) is unsatisfiable if its equations have no unifier.

Definition 7.9.2 (MUS; minimum error source)

A minimal unsatisfiable subset (MUS) of \(S\) is an unsatisfiable \(M \subseteq S\) such that every proper subset of \(M\) is satisfiable. A correction set is a set \(L\) of locations such that removing every constraint with a location in \(L\) makes \(S\) satisfiable. A minimum error source is a correction set of minimum size.

Lemma 7.9.3 (Correction sets hit every MUS)

\(L\) is a correction set iff \(L \cap \mathrm{locs}(M) \ne \emptyset\) for every MUS \(M\) of \(S\). Hence the minimum error sources are the minimum hitting sets of \(\{\mathrm{locs}(M)\}\).

Proof

(\(\Rightarrow\)) If some MUS \(M\) had no location in \(L\), removing \(L\)'s constraints would keep all of \(M\), which is unsatisfiable. (\(\Leftarrow\)) Suppose \(L\) hits every MUS but the remaining set \(S'\) is unsatisfiable. Every unsatisfiable finite set contains an MUS (remove constraints one at a time while it stays unsatisfiable; the process stops at a minimal one). That MUS lies in \(S'\), so it contains no constraint located in \(L\) — contradicting that \(L\) hits it.

Blame by traversal order¶

Algorithm 7.9.4 (Labelled constraint generation, and first-failure blame)

Input: a let-free MiniML expression \(e\) (lets can be expanded, Lesson 7.3).
Output: a list of labelled constraints in traversal order; first-failure blame reports the label of the first constraint whose addition makes the prefix unsatisfiable.
Precondition: labels are the positions of the subterms (the lab's convention, SPEC §2.2).
Postcondition: the constraints are satisfiable iff \(e\) is typable (Theorem 7.4.8); the reported label belongs to some MUS (Proposition 7.9.7).
Invariant: the prefix of constraints processed so far is satisfiable.

function Gen(Γ, e, τ):                                     # M-style: τ is expected
    case e of
        n / b / ():         emit (pos(e), τ = int / bool / unit)
        x:                  emit (pos(e), τ = Γ(x))               # or an instance of a builtin
        fun x -> e1:        α, β fresh;  emit (pos(e), τ = α → β);  Gen(Γ[x ↦ α], e1, β)
        e1 e2:              α fresh;  Gen(Γ, e1, α → τ);  Gen(Γ, e2, α)
        if e1 then e2 else e3:   Gen(Γ, e1, bool);  Gen(Γ, e2, τ);  Gen(Γ, e3, τ)
        (e1, e2):           α, β fresh;  emit (pos(e), τ = α × β);  Gen(Γ, e1, α);  Gen(Γ, e2, β)
        e1 ⊕ e2:            emit (pos(e), τ = τ⊕);  Gen(Γ, e1, int);  Gen(Γ, e2, int)
function FirstFailure(cs):
    θ ← []
    for (ℓ, c) in cs:  if Unify(θc) fails: return ℓ;  θ ← MGU ∘ θ
    return "typable"

Minimal unsatisfiable constraint sets¶

Algorithm 7.9.5 (One MUS by deletion; all MUSes; minimum error sources)

Input: an unsatisfiable list of labelled constraints \(S = \langle s_0, \dots, s_{m-1} \rangle\).
Output: DeletionMUS: one MUS; AllMUS: every MUS; MinSources: every minimum error source.
Precondition: satisfiability of a set is decided by unification (Lesson 7.1).
Postcondition: as named (Theorem 7.9.8).
Invariant (DeletionMUS): the kept set \(K\) is unsatisfiable, and every constraint already examined and kept is necessary for the unsatisfiability of \(K\).

function DeletionMUS(S):
    K ← S
    for i in 0..m-1:
        if Unsat(K \ {s_i}):  K ← K \ {s_i}          # s_i not needed: drop it
    return K
function AllMUS(S):                                   # exhaustive, for small S
    found ← []
    for k in 1..m:  for each k-subset T of S:
        if no M in found is ⊆ T and Unsat(T): add T to found
    return found
function MinSources(S):
    muses ← AllMUS(S);  labels ← ⋃ locs(M)
    for k in 1..|labels|:
        H ← all k-subsets of labels that intersect locs(M) for every M in muses
        if H ≠ []: return H                             # Lemma 7.9.3

Provenance notes¶

Algorithm 7.9.6 (Unification with provenance, as in Pebble's E0416)

Input: a union-find unifier (Algorithm 7.1.10) extended with an origin per class.
Output: on failure, the failing location and the origin of the binding it conflicts with.
Precondition: every call Unify(τ1, τ2, ℓ) carries the location \(\ell\) of the constraint.
Postcondition: the origin of a bound class is the location of the constraint that first bound it (Proposition 7.9.9).
Invariant: unbound classes have no origin; a class's origin never changes once set.

function Unify(τ1, τ2, ℓ):
    if τ1 is an unbound class ν and τ2 is a type t:  bind ν to t;  origin(ν) ← ℓ
    (other cases as Algorithm 7.1.10; merging two unbound classes sets no origin)
function Report(τ1, τ2, ℓ):                    # called when Unify fails
    if one side came from a name x whose class ν has origin o, and a fresh class would unify:
        error E0416 at ℓ;  note "x is inferred to have type … because of this" at o
    else: error at ℓ with the §13.3 code

3. Worked example¶

Running example (MiniML, one line; the lab corpus's positions): fun x -> (if x then 0 else 1, (x + 1, x * 2)). The programmer most likely meant x to be an integer and wrote if x by mistake. Algorithm 7.9.4 generates 12 labelled constraints (the oracle hm.labelled_constraints):

#	label	reason	constraint
0	1:1	function	\(t_1 = t_2 \to t_3\)
1	1:10	pair	\(t_3 = t_4 \times t_5\)
2	1:14	use of `x` (condition)	\(\mathsf{bool} = t_2\)
3	1:21	literal `0`	\(t_4 = \mathsf{int}\)
4	1:28	literal `1`	\(t_4 = \mathsf{int}\)
5	1:31	pair	\(t_5 = t_7 \times t_8\)
6	1:34	result of `+`	\(t_7 = \mathsf{int}\)
7	1:32	use of `x` (operand of `+`)	\(\mathsf{int} = t_2\)
8	1:36	literal `1`	\(\mathsf{int} = \mathsf{int}\)
9	1:41	result of `*`	\(t_8 = \mathsf{int}\)
10	1:39	use of `x` (operand of `*`)	\(\mathsf{int} = t_2\)
11	1:43	literal `2`	\(\mathsf{int} = \mathsf{int}\)

Blame by traversal order¶

The prefix \(\langle 0, \dots, 6 \rangle\) is satisfiable with \(t_2 = \mathsf{bool}\); constraint 7 fails: blame 1:32, the x in x + 1. W, J and M all report 1:32 (hm.infer). OCaml and GHC blame the same place (§7).

Minimal unsatisfiable constraint sets¶

DeletionMUS examines constraints 0–11 in order; dropping 0–1 and 3–9 and 11 keeps the rest unsatisfiable, dropping 2 or 10 would not:

i	\(K \setminus \{s_i\}\) unsatisfiable?	action	K afterwards
0, 1	yes	drop	\(\{2, \dots, 11\}\)
2	no (no `bool` left)	keep	unchanged
3–9	yes (7 is dropped too: 10 still conflicts with 2)	drop	\(\{2, 10, 11\}\)
10	no	keep	unchanged
11	yes	drop	\(\{2, 10\}\)

So one MUS is \(\{2, 10\}\) = {1:14, 1:39}. AllMUS finds exactly two: \(\{2, 7\}\) and \(\{2, 10\}\) (location sets {1:14, 1:32} and {1:14, 1:39}). The minimum hitting set is the single location 1:14 — the x in if x, which appears in both explanations. Changing it (e.g. to if x > 0) fixes the program; changing the blamed 1:32 does not.

Provenance notes¶

With provenance (Algorithm 7.9.6), traversal order still blames 1:32, but the message can cite the origin of \(t_2 = \mathsf{bool}\): "x is inferred to have type bool because of this" at 1:14 — exactly Pebble's E0416 form, and the location the MUS analysis found. The Pebble version is the file err-infer.pbl of tests/ch07/Inputs (Lesson 7.6 §3): E0416 at the second conflicting use, the note at the first.

4. Invariants and correctness¶

Blame by traversal order¶

Proposition 7.9.7 (First-failure blame lies in an MUS, but not necessarily in a minimum error source)

If FirstFailure reports the constraint \(s_j\), then \(s_j\) belongs to some MUS of \(\langle s_0, \dots, s_j \rangle\) (hence of \(S\)). The label of \(s_j\) need not belong to any minimum error source.

Proof

The prefix \(P = \langle s_0, \dots, s_{j-1} \rangle\) is satisfiable and \(P \cup \{s_j\}\) is not. Apply DeletionMUS to \(P \cup \{s_j\}\) with \(s_j\) examined last: every MUS it can return must contain \(s_j\), because any subset of \(P\) is satisfiable. That MUS is also an MUS of \(S\) (minimality is a property of the subset alone). For the second statement, the running example: first-failure reports 1:32, and the only minimum error source is {1:14}.

Minimal unsatisfiable constraint sets¶

Theorem 7.9.8 (Correctness of Algorithm 7.9.5)

DeletionMUS returns an MUS of \(S\); AllMUS returns exactly the MUSes of \(S\); MinSources returns exactly the minimum error sources.

Proof

DeletionMUS: invariant — \(K\) is unsatisfiable (initially \(S\); a drop happens only when the smaller set is unsatisfiable). At the end, suppose some \(s_i \in K\) could be removed with \(K \setminus \{s_i\}\) unsatisfiable. When \(s_i\) was examined, the then-current \(K_i \supseteq K\) satisfied "\(K_i \setminus \{s_i\}\) is satisfiable" (otherwise \(s_i\) would have been dropped); but \(K \setminus \{s_i\} \subseteq K_i \setminus \{s_i\}\) and subsets of satisfiable sets are satisfiable — contradiction. So \(K\) is minimal. AllMUS: subsets are enumerated by increasing size, and a set \(T\) is recorded iff it is unsatisfiable and contains no recorded set. If \(T\) is an MUS, none of its proper subsets is unsatisfiable, so it contains no recorded set and is recorded. If \(T\) is unsatisfiable but not minimal, it has a proper unsatisfiable subset, which contains an MUS \(M\) with \(\lvert M \rvert < \lvert T \rvert\); \(M\) was recorded earlier, so \(T\) is skipped. MinSources: by Lemma 7.9.3, enumerating location sets by increasing size and keeping those that hit every MUS yields exactly the minimum ones.

Provenance notes¶

Proposition 7.9.9 (The origin explains the conflict)

In Algorithm 7.9.6, if Unify(τ1, τ2, ℓ) fails because a class \(\nu\) is bound to \(t\) with origin \(o\), and a fresh class would have unified, then the constraints at \(o\) and at \(\ell\), together with the equations that connect the two occurrences of \(\nu\), form an unsatisfiable set; in particular \(\{o, \ell\}\) is contained in the locations of an MUS.

Proof

The binding \(\nu \mapsto t\) was caused by the constraint at \(o\) (the origin is set exactly then and never changed). The failing constraint at \(\ell\) requires \(\nu\) (reached from \(\tau_1\) or \(\tau_2\) through merges, each a constraint of the program) to equal a type \(t' \neq t\) — "a fresh class would have unified" rules out conflicts that do not involve \(\nu\). The constraint at \(o\), the one at \(\ell\), and the merge equations are therefore unsatisfiable together; any MUS extracted from them by deletion must keep \(o\) and \(\ell\), since without \(o\) the class is free and without \(\ell\) nothing contradicts \(t\).

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Blame by traversal order	free: part of inference (\(O(m\,\alpha(m))\))	free	none	\(m\) constraints
One MUS by deletion	\(m\) satisfiability checks: \(O(m^2\,\alpha(m))\)	small \(m\) after slicing	\(O(m)\)	\(m\) constraints
All MUSes / minimum error sources	exponential: up to \(\binom{m}{m/2}\) MUSes; minimum hitting set is NP-hard	seconds with MaxSMT solvers on real programs [PKW14]	exponential	\(m\) constraints
Provenance notes	\(O(1)\) per binding	free	one location per class	classes

Justification. Deletion performs one satisfiability test per constraint, each a unification run. The number of MUSes can be exponential: \(m/2\) independent pairs of conflicting alternatives give \(2^{m/2}\) MUSes. Minimum hitting set generalizes vertex cover.

Pathological family. \(x\) used as bool once and as int at \(k\) places (the running example with \(k\) arithmetic uses) has exactly \(k\) MUSes \(\{\)cond\(, \mathrm{use}_i\}\), and traversal-order blame reports whichever use comes first after the condition — so the reported location is wrong for every \(k \ge 2\) while the minimum error source is always the one condition. With the uses before the condition, traversal blames the condition: the verdict depends only on the order.

Blame by traversal order¶

Algorithm M / expected types (Lesson 7.2): blame the leaf that contradicts the expectation. Trade-off: earlier, often better locations; still order-dependent.
Reordering the traversal (McAdam's symmetric unification [McA98]): unify the substitutions of sibling subterms symmetrically so no side is privileged. Trade-off: removes the left-to-right bias; still reports one point.

Minimal unsatisfiable constraint sets¶

Type error slicing [HW04]: report all locations of an MUS, highlighted. Trade-off: complete explanation; long for large programs.
Ranking by likelihood (SHErrLoc [ZM14]): a Bayesian score that prefers locations with few conflicting and many satisfied constraints. Trade-off: better guesses in practice; heuristic.
MaxSMT with weights [PKW14]: weight each location (e.g. by the size of the subterm) and ask an SMT solver for a minimum-weight correction set. Trade-off: optimal by the chosen metric; needs an external solver.

Provenance notes¶

Evidence chains (GHC's CtOrigin, rustc's ObligationCause): keep a chain of "arising from" steps. Trade-off: rich messages; must be pruned to stay readable.
Blame the binding, not the use (Pebble's E0416 choice): name the variable whose type was requested twice. Trade-off: points at a declaration the programmer can annotate; may be two steps from the actual typo.

7. In real compilers¶

Blame by traversal order¶

OCaml and GHC both report the first failing constraint in their traversal order — Typecore.type_expect [OCAML-Typecore] and GHC's solver with its CtOrigin [GHC-Solver] — and so both blame the running example's x + 1.

Order-dependent blame in OCaml 4.14 and GHC 9.4

Reproduce (OCaml 4.14.1, GHC 9.4.7):

mkdir -p ml hs
echo 'let f = fun x -> ((if x then 0 else 1), (x + 1, x * 2))' > ml/loc.ml
ocamlc -i ml/loc.ml
echo 'f x = (if x then 0 else 1, (x + 1, x * 2))' > hs/Loc.hs
LC_ALL=C ghc -fno-code hs/Loc.hs

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

File "ml/loc.ml", line 1, characters 41-42:
1 | let f = fun x -> ((if x then 0 else 1), (x + 1, x * 2))
                                             ^
Error: This expression has type bool but an expression was expected of type
         int
hs/Loc.hs:1:31: error:
    * Could not deduce (Num Bool) arising from a use of `+'
      from the context: Num a
        bound by the inferred type of
                   f :: Num a => Bool -> (a, (Bool, Bool))
        at hs/Loc.hs:1:1-42
    * In the expression: x + 1
      In the expression: (x + 1, x * 2)
      In the expression: (if x then 0 else 1, (x + 1, x * 2))
  |
1 | f x = (if x then 0 else 1, (x + 1, x * 2))
  |                               ^

What to notice: both compilers decided x : bool at the condition and blame the next use, x + 1 — first-failure blame (Proposition 7.9.7). GHC's inferred type Bool -> (a, (Bool, Bool)) even shows how far it trusted the condition. The minimum error source of §3 is the condition itself. (OCaml needs parentheses around the if, which otherwise extends over the tuple.)

Minimal unsatisfiable constraint sets¶

No mainstream compiler computes MUSes by default; SHErrLoc [ZM14] and MinErrLoc [PKW14] are research implementations for OCaml and Haskell. The course's oracle hm.all_mus / hm.minimum_error_sources computes them for MiniML.

The running example's MUSes, from the course oracle

Reproduce (Python 3.11 from the course's uv environment; run from the repository root):

cd tools && uv run python -c "
from course.lib import hm
cs = hm.labelled_constraints(hm.parse('fun x -> (if x then 0 else 1, (x + 1, x * 2))'))
muses = hm.all_mus(cs)
print([[cs[i][0] for i in m] for m in muses])
print(hm.minimum_error_sources(cs, muses))
print(hm.infer('fun x -> (if x then 0 else 1, (x + 1, x * 2))', 'W'))"

Output (complete):

[['1:14', '1:32'], ['1:14', '1:39']]
[('1:14',)]
('error', 'mismatch', '1:32')

What to notice: two MUSes, one shared location: the condition at 1:14 is the minimum error source, while W reports 1:32 — the table of §3, and the gap Proposition 7.9.7 predicts.

Provenance notes¶

rustc attaches an ObligationCause to every obligation and prints "expected due to this" / "expected because this is …" (Lesson 6.4's box) [RUSTC-Typeck]; GHC prints "arising from a use of …"; Pebble's inferTypes stores one origin per numeric class (Solver::originOf in the reference) for E0416's note.

Provenance in rustc 1.94 and in Pebble's inference mode

Reproduce (rustc 1.94.1; the course's reference build with build/<preset>/bin on the PATH):

mkdir -p rs && cat > rs/conflict.rs <<'EOF'
fn main() {
    let n = 1;
    let a: u8 = n;
    let b: u64 = n;
    println!("{} {}", a, b);
}
EOF
rustc --edition 2021 rs/conflict.rs -o rs/conflict
cat > conflict.pbl <<'EOF'
fn main() -> int {
    let n = 1;
    let a: int = n;
    let b: float = n;
    return 0;
}
EOF
ch07-infer conflict.pbl | grep -E 'error|note'

Output (complete):

error[E0308]: mismatched types
 --> rs/conflict.rs:4:18
  |
4 |     let b: u64 = n;
  |            ---   ^ expected `u64`, found `u8`
  |            |
  |            expected due to this
  |
help: you can convert a `u8` to a `u64`
  |
4 |     let b: u64 = n.into();
  |                   +++++++

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0308`.
4:20: error[E0416]: cannot infer the type of 'n'; add a type annotation
3:18: note: 'n' is inferred to have type 'int' because of this

What to notice: rustc blames the second use and cites the origin of the expected type (the annotation u64), but not why n became u8. Pebble's E0416 cites the other half: the use that decided n : int (Algorithm 7.9.6). Together the two notes are the MUS {3:18, 4:20}.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
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

Choose traversal-order blame plus provenance for a production compiler: it is free and, with the origin of the conflicting binding, usually enough. Add MUS-based localization in an IDE or for teaching, where seconds per error are affordable and the best guess matters most.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Blame by traversal order	`blame-first-failure`, `m-error-position`	`hm-trace` (the error positions of ill-typed programs, `--difficulty hard`)	`traversal-blame`	lab L1, L3 (error headers)
Minimal unsatisfiable constraint sets	`mus-count`, `min-error-source`	— (the quiz items are computed with `hm.all_mus`; the MUS search is exhaustive and slow for a drill's random programs)	`mus-localization`	—
Provenance notes	`provenance-note`, `pebble-e0416`	— (exercise E3's tests)	`provenance`	E3

References¶

See the chapter references.

Lesson 7.9 — Error localization in type inference¶

1. Problem and motivation¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

2. Definitions and algorithms¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

3. Worked example¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

4. Invariants and correctness¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

5. Complexity¶

6. Variants and refinements¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

7. In real compilers¶

Blame by traversal order¶

Minimal unsatisfiable constraint sets¶

Provenance notes¶

8. Comparison¶

9. Assessment¶

References¶