Type Checking & Inference in Compilers

The language of type systems is the typing judgment. A typing judgment is a formal statement of the form:

Γ ⊢ e : τ

Read: "Under type environment Γ, expression e has type τ." The symbol ⊢ (turnstile) separates the context (what we know) from the claim (what we are asserting). This notation is borrowed directly from proof theory, and for good reason: a type checker is a proof-checker.

Breaking down each part:

• Γ (gamma) is the type environment — a finite mapping from variable names to types, like {x: Int, f: Int → Bool}. It tracks what is in scope.
• e is any expression: a literal, a variable reference, a function call, a let binding, etc.
• τ (tau) is the claimed type, drawn from the language's type algebra (e.g., Int, Bool, Int → Int, List<String>).

A typing judgment is valid if it can be derived from the language's type rules. The type checker's job is to verify these derivations. Crucially, if you cannot derive Γ ⊢ e : τ for any τ, then e is ill-typed — a type error.

Analogy: think of Γ as the set of hypotheses in a proof, e as a proposition you want to prove, and τ as the conclusion. The type rules are your axioms and inference rules.

-- Haskell-style notation
-- Γ = {x : Int, y : Bool}
-- Judgment: Γ ⊢ (x + 1) : Int
--
-- We can derive this because:
--   1. Γ ⊢ x : Int       (by VAR rule, x ∈ Γ)
--   2. Γ ⊢ 1 : Int       (by LIT rule)
--   3. Γ ⊢ (x + 1) : Int (by ADD rule, from 1 and 2)

A type rule specifies the conditions under which a typing judgment holds. It is written in natural-deduction style:

  premise₁   premise₂   …
─────────────────────────── [RULE-NAME]
         conclusion

If all premises hold, the conclusion holds. The premises are themselves typing judgments (or side conditions like "τ₁ = τ₂").

Core rules for a simple expression language:

VAR — a variable has the type the environment says it has:

  x : τ ∈ Γ
────────────── [VAR]
  Γ ⊢ x : τ

LIT — integer literals are Int:

─────────────────── [LIT-INT]
  Γ ⊢ n : Int

ADD — addition requires both operands to be Int and produces Int:

  Γ ⊢ e₁ : Int    Γ ⊢ e₂ : Int
─────────────────────────────────── [ADD]
       Γ ⊢ e₁ + e₂ : Int

IF — a conditional requires a Bool guard and both branches must agree in type:

  Γ ⊢ e₁ : Bool    Γ ⊢ e₂ : τ    Γ ⊢ e₃ : τ
─────────────────────────────────────────────── [IF]
          Γ ⊢ if e₁ then e₂ else e₃ : τ

ABS — lambda abstraction extends the environment:

  Γ, x : τ₁ ⊢ e : τ₂
────────────────────────── [ABS]
  Γ ⊢ λx:τ₁. e : τ₁ → τ₂

APP — function application:

  Γ ⊢ e₁ : τ₁ → τ₂    Γ ⊢ e₂ : τ₁
──────────────────────────────────────── [APP]
          Γ ⊢ e₁ e₂ : τ₂

These rules form a compositional system: the type of a complex expression is determined entirely by the types of its subexpressions and the rule that applies. This compositionality is what makes the recursive algorithm tractable.

A derivation tree (also called a type derivation or proof tree) is the tree of rule applications that proves a judgment. If you can construct such a tree, the expression type-checks; if you cannot, it does not.

-- Derivation tree for: {} ⊢ (λx:Int. x + 1) 5 : Int
--
--  [VAR] x:Int ⊢ x:Int   [LIT-INT] x:Int ⊢ 1:Int
--  ──────────────────────────────────────────────── [ADD]
--             x:Int ⊢ x+1 : Int
--  ──────────────────────────────── [ABS]
--   {} ⊢ (λx:Int. x+1) : Int→Int       [LIT-INT] {} ⊢ 5 : Int
--  ─────────────────────────────────────────────────────────── [APP]
--                  {} ⊢ (λx:Int. x+1) 5 : Int

The type environment Γ is the formal model of scope. It maps names to types for every identifier currently in scope. As the type checker descends the AST, it extends Γ when entering a new binding (function parameter, let binding, class field declaration) and contracts it when leaving that scope.

Key operations:

• Γ(x) — look up the type of x in Γ (fails if x is not in scope → "undeclared variable" error)
• Γ, x : τ — create a new environment extending Γ with the binding x → τ (used in ABS, LET rules)
• For block-scoped languages (C, Java), Γ is a stack of maps, one per lexical scope level

Let bindings and type environments:

  Γ ⊢ e₁ : τ₁     Γ, x : τ₁ ⊢ e₂ : τ₂
────────────────────────────────────────── [LET]
        Γ ⊢ let x = e₁ in e₂ : τ₂

The let rule first types e₁ under the current Γ, then types e₂ under an extended Γ that includes x : τ₁. The scope of x is exactly e₂.

Implementation: In a real compiler, Γ is typically a symbol table — a hash map or a functional red-black tree (the latter supports efficient persistent extension without copying, which matters for inference).

Shadowing: The notation Γ, x : τ means the new binding takes precedence. If x was already in Γ, the inner binding shadows the outer one within the scope of the let body.

# Python-style symbol table implementation
from dataclasses import dataclass, field
from typing import Optional

@dataclass
class TypeEnv:
    """Persistent functional type environment (linked list of frames)."""
    bindings: dict = field(default_factory=dict)
    parent: Optional['TypeEnv'] = None

    def extend(self, name: str, typ: str) -> 'TypeEnv':
        """Return a new environment with name:typ added."""
        new_env = TypeEnv(parent=self)
        new_env.bindings[name] = typ
        return new_env

    def lookup(self, name: str) -> str:
        if name in self.bindings:
            return self.bindings[name]
        if self.parent is not None:
            return self.parent.lookup(name)
        raise TypeError(f"Undeclared variable: {name}")

# Usage:
env = TypeEnv()
env = env.extend('x', 'Int')
env = env.extend('f', 'Int -> Bool')
print(env.lookup('x'))  # 'Int'
print(env.lookup('f'))  # 'Int -> Bool'

A type checker is a recursive function that walks the AST and, at each node, applies the matching type rule. The algorithm is syntax-directed: each AST node kind has exactly one applicable rule (in most deterministic type systems), so the case analysis is on the node kind.

Algorithm sketch for a simple expression language:

function typecheck(env, expr):
    match expr:
        case Lit(n):     return Int
        case Bool(b):    return Bool
        case Var(x):     return env.lookup(x)   # raises if not in scope
        case Add(e1,e2): expect(typecheck(env,e1), Int)
                         expect(typecheck(env,e2), Int)
                         return Int
        case If(c,t,f):  expect(typecheck(env,c), Bool)
                         τ = typecheck(env, t)
                         expect(typecheck(env,f), τ)
                         return τ
        case Lam(x,τ,e): return typecheck(env.extend(x,τ), e) → τ
        case App(f,a):   tf = typecheck(env, f)   # must be τ1→τ2
                         ta = typecheck(env, a)   # must be τ1
                         expect_arrow(tf, ta)
                         return tf.codomain
        case Let(x,e1,e2): τ1 = typecheck(env, e1)
                           return typecheck(env.extend(x,τ1), e2)

This is O(n) in the AST size for most simply-typed languages — each node is visited once. The recursion mirrors the structure of the derivation tree.

Key design property — type safety (progress + preservation):

• Progress: a well-typed closed expression is not stuck (it can always take a step, or it is already a value)
• Preservation (subject reduction): if Γ ⊢ e : τ and e → e', then Γ ⊢ e' : τ

These two properties together guarantee that well-typed programs do not get stuck at runtime — the formal statement of "well-typed programs do not go wrong" (Milner, 1978).

# Minimal type checker for arithmetic + booleans + let
from __future__ import annotations
from dataclasses import dataclass
from typing import Union

# --- AST nodes ---
@dataclass
class Lit:   value: int
@dataclass
class BoolLit: value: bool
@dataclass
class Var:   name: str
@dataclass
class Add:   left: Expr; right: Expr
@dataclass
class If:    cond: Expr; then_: Expr; else_: Expr
@dataclass
class Let:   name: str; val: Expr; body: Expr

Expr = Union[Lit, BoolLit, Var, Add, If, Let]

def typecheck(env: TypeEnv, expr: Expr) -> str:
    if isinstance(expr, Lit):     return 'Int'
    if isinstance(expr, BoolLit): return 'Bool'
    if isinstance(expr, Var):     return env.lookup(expr.name)
    if isinstance(expr, Add):
        t1 = typecheck(env, expr.left)
        t2 = typecheck(env, expr.right)
        if t1 != 'Int' or t2 != 'Int':
            raise TypeError(f'Add expects Int+Int, got {t1}+{t2}')
        return 'Int'
    if isinstance(expr, If):
        tc = typecheck(env, expr.cond)
        if tc != 'Bool':
            raise TypeError(f'If condition must be Bool, got {tc}')
        tt = typecheck(env, expr.then_)
        te = typecheck(env, expr.else_)
        if tt != te:
            raise TypeError(f'If branches disagree: {tt} vs {te}')
        return tt
    if isinstance(expr, Let):
        tv = typecheck(env, expr.val)
        return typecheck(env.extend(expr.name, tv), expr.body)
    raise ValueError(f'Unknown node: {expr}')

# Test:
e = Let('x', Lit(3), Add(Var('x'), Lit(1)))
print(typecheck(TypeEnv(), e))  # 'Int'

Expressions return a value; statements (in imperative languages) are executed for their side effects. Type checking statements requires a slightly different treatment: instead of returning a type, the checker often returns an updated type environment and/or a statement type like Unit (nothing).

Checking assignment:

  Γ ⊢ e : τ    Γ(x) = τ
─────────────────────────── [ASSIGN]
    Γ ⊢ x = e : Unit

The right-hand side type must match the declared type of x. In languages with subtyping, we check that τ_rhs is a subtype of τ_lhs.

Checking while loops:

  Γ ⊢ e : Bool    Γ ⊢ s : Unit
────────────────────────────────── [WHILE]
    Γ ⊢ while e do s : Unit

Checking function bodies (return type): For a function declared as returning type τ, every return e statement in the body must satisfy Γ ⊢ e : τ. A common implementation strategy:

• Push the declared return type onto a return-type stack when entering a function
• When checking a return statement, pop the stack and verify the expression type

Checking entire programs: A class or module is checked by building an initial Γ from all top-level declarations (a pre-pass or forward declaration scan), then type-checking each declaration body. This pre-pass is what allows mutually recursive functions without forward declarations.

Type checking vs. type inference distinction in practice: In a checking regime (Java, C++), the programmer annotates types and the checker verifies. In an inference regime (Haskell, OCaml), the checker can also deduce missing annotations. Most modern languages (Rust, TypeScript, Kotlin) do bidirectional type checking — a blend where annotations propagate expectations downward while synthesis propagates types upward.

# Checking a simple imperative statement block
# Statement types: Assign, While, Return, Block

@dataclass
class Assign: name: str; expr: Expr
@dataclass
class While:  cond: Expr; body: 'Stmt'
@dataclass
class Return: expr: Expr
@dataclass
class Block:  stmts: list

def check_stmt(env: TypeEnv, stmt, return_type: str) -> TypeEnv:
    """Returns (possibly extended) env; raises TypeError on failure."""
    if isinstance(stmt, Assign):
        declared = env.lookup(stmt.name)
        actual   = typecheck(env, stmt.expr)
        if actual != declared:
            raise TypeError(
                f"Cannot assign {actual} to {stmt.name}:{declared}")
        return env
    if isinstance(stmt, While):
        tc = typecheck(env, stmt.cond)
        if tc != 'Bool':
            raise TypeError(f'While guard must be Bool, got {tc}')
        check_stmt(env, stmt.body, return_type)
        return env
    if isinstance(stmt, Return):
        tr = typecheck(env, stmt.expr)
        if tr != return_type:
            raise TypeError(
                f'Return type {tr} != declared {return_type}')
        return env
    if isinstance(stmt, Block):
        for s in stmt.stmts:
            env = check_stmt(env, s, return_type)
        return env
    raise ValueError(f'Unknown statement: {stmt}')

An attribute grammar is a formal framework for attaching semantic information — including types — to parse tree nodes. Introduced by Donald Knuth in 1968, it extends a CFG by decorating each grammar symbol with attributes, and each production with semantic rules that compute attribute values.

Two kinds of attributes:

• Synthesized attributes flow upward (from children to parent). The type of an expression is a classic synthesized attribute: it is computed from the types of subexpressions.
• Inherited attributes flow downward (from parent or siblings to a child). The type environment Γ passed into a subexpression is a classic inherited attribute: it flows from the enclosing scope.

Example — a simple expression grammar:

Production: E → E₁ + E₂
Semantic rules:
  E.type = if E₁.type == Int and E₂.type == Int
           then Int
           else TypeError
  E₁.env = E.env   (inherited: pass environment down)
  E₂.env = E.env

S-attributed and L-attributed grammars:

• S-attributed: only synthesized attributes. Can be evaluated bottom-up in a single pass (ideal for LR parsing).
• L-attributed: inherited attributes may depend only on attributes of symbols to the left in the production (and on inherited attributes of the parent). Can be evaluated top-down / in a single left-to-right pass (ideal for LL parsing).

Type checking fits naturally into an L-attributed scheme: Γ is inherited top-down (passing scope information to children), while the computed type is synthesized bottom-up (computed from subexpressions).

Practical use: Most production compilers do not literally implement Knuth attribute grammars. Instead, the equivalent computation is expressed as recursive passes over the AST. But the attribute grammar framework is the theoretical justification for why such passes are well-defined and terminating.

-- Attribute grammar notation (pseudocode / Knuth-style)
--
-- Grammar:
--   E  → E + T   | T
--   T  → num     | ( E )
--
-- Attributes:
--   E.type  : synthesized (computed bottom-up)
--   E.env   : inherited   (passed top-down)
--
-- Production: E → E₁ + T
--   Semantic rules:
--     E₁.env  = E.env                  -- pass env down left child
--     T.env   = E.env                  -- pass env down right child
--     E.type  = if E₁.type = Int       -- synthesize up
--                  and T.type = Int
--               then Int
--               else TypeError
--
-- Production: T → num
--   Semantic rules:
--     T.type  = Int                    -- base case, no env needed

Type inference allows programs to be written without explicit type annotations; the compiler deduces them. The classic algorithm, due to Hindley (1969) and Milner (1978), works in two phases:

Phase 1 — Constraint generation: Walk the AST. For each node, introduce a fresh type variable (α, β, γ, …) if the type is unknown, and emit a type constraint (an equation between types) based on the applicable type rule.

For let x = e₁ in e₂:

• Let α = type(x), infer type(e₁) = τ₁, add constraint α = τ₁
• Infer type(e₂) = τ₂, result type = τ₂

For e₁ e₂ (application):

• Let type(e₁) = τ₁, type(e₂) = τ₂, result type = α (fresh)
• Add constraint τ₁ = τ₂ → α (e₁ must be a function from τ₂ to α)

For e₁ + e₂:

• Add constraints type(e₁) = Int, type(e₂) = Int, result = Int

Phase 2 — Unification (solving constraints): The set of constraints is a system of type equations. Unification (Robinson, 1965) solves them:

• If both sides are the same type constant (Int = Int): succeed
• If one side is a type variable α: substitute α ↦ τ everywhere
• If both sides are type constructors (τ₁ → τ₂ = σ₁ → σ₂): recursively unify τ₁=σ₁ and τ₂=σ₂
• If both sides are different type constants (Int = Bool): type error — unification fails
• Occurs check: if α appears in τ, the constraint α = τ would produce infinite types — fail

The substitution produced by unification is the principal type of the expression: the most general type consistent with the constraints.

# Constraint generation for a tiny language
from itertools import count

counter = count()
def fresh(): return f"α{next(counter)}"

class Constraint:
    def __init__(self, lhs, rhs): self.lhs, self.rhs = lhs, rhs
    def __repr__(self): return f"{self.lhs} = {self.rhs}"

def infer(env: dict, expr) -> tuple:
    """Returns (type, list[Constraint])."""
    constraints = []
    if isinstance(expr, Lit):
        return 'Int', []
    if isinstance(expr, Var):
        if expr.name not in env:
            raise TypeError(f'Unbound: {expr.name}')
        return env[expr.name], []
    if isinstance(expr, Add):
        t1, c1 = infer(env, expr.left)
        t2, c2 = infer(env, expr.right)
        constraints = c1 + c2 + [
            Constraint(t1, 'Int'),
            Constraint(t2, 'Int')
        ]
        return 'Int', constraints
    if isinstance(expr, Lam):   # Lam(param, body), no annotation
        α = fresh()
        β = fresh()
        t_body, c_body = infer({**env, expr.param: α}, expr.body)
        constraints = c_body + [Constraint(β, t_body)]
        return f'{α} -> {β}', constraints
    if isinstance(expr, App):
        t_fun, c_fun = infer(env, expr.func)
        t_arg, c_arg = infer(env, expr.arg)
        α = fresh()
        constraints = c_fun + c_arg + [
            Constraint(t_fun, f'{t_arg} -> {α}')
        ]
        return α, constraints
    raise ValueError(f'Unknown: {expr}')

# Example: infer type of (λx. x + 1)
# Generates: α0 = Int, α1 = Int
# Unification gives: x:Int, result:Int → type = Int→Int

Unification is the algorithmic heart of type inference. Given a set of type equations, unification finds the most general unifier (MGU) — a substitution S such that applying S to both sides of every equation makes them identical.

Robinson's unification algorithm (1965):

function unify(constraints, substitution):
    if constraints is empty: return substitution
    take first constraint (τ₁, τ₂)
    apply current substitution: τ₁ = apply(sub, τ₁), τ₂ = apply(sub, τ₂)
    if τ₁ == τ₂:  -- identical, skip
        return unify(rest, substitution)
    if τ₁ is type-variable α:
        if α occurs in τ₂: FAIL (occurs check)
        sub' = sub extended with α ↦ τ₂
        return unify(apply(sub', rest), sub')
    if τ₂ is type-variable α: symmetric case
    if τ₁ = C(σ₁,...,σn) and τ₂ = C(σ₁',...,σn'):  -- same constructor
        return unify({σ₁=σ₁',...,σn=σn'} ∪ rest, substitution)
    FAIL (type error: incompatible constructors)

Why the occurs check matters: Without it, α = α → Int would give α = (α → Int) → Int = ((α→Int)→Int) → Int = … — an infinite type. The occurs check catches this and rejects it. (Note: Haskell has a flag UndecidableInstances / NoMonomorphismRestriction that relates to this, and Prolog typically omits the occurs check for performance.)

Complexity: Naive Robinson is O(n²) in the number of constraints. Paterson and Wegman (1978) showed it can be done in nearly linear time using a union-find (disjoint-set union) data structure. This is the algorithm used in production ML compilers.

What unification produces: The substitution S is a map from type variables to types. After unification, apply S to the inferred type of the whole program to get the principal type — the most general type the expression can have.

def unify(constraints: list, subst: dict) -> dict:
    """Returns most-general unifier (substitution dict)."""
    if not constraints:
        return subst
    (lhs, rhs), *rest = constraints
    lhs = apply_subst(subst, lhs)
    rhs = apply_subst(subst, rhs)
    if lhs == rhs:
        return unify(rest, subst)
    if is_typevar(lhs):
        if occurs_in(lhs, rhs):
            raise TypeError(f'Occurs check: {lhs} in {rhs}')
        new_sub = {lhs: rhs, **{k: apply_subst({lhs: rhs}, v)
                                 for k, v in subst.items()}}
        return unify([(apply_subst({lhs:rhs}, l),
                       apply_subst({lhs:rhs}, r))
                      for l,r in rest], new_sub)
    if is_typevar(rhs):
        return unify([(rhs, lhs)] + rest, subst)  # symmetric
    # Both are type constructors: decompose
    if head(lhs) == head(rhs) and arity(lhs) == arity(rhs):
        new_constraints = list(zip(args(lhs), args(rhs))) + rest
        return unify(new_constraints, subst)
    raise TypeError(f'Cannot unify {lhs} with {rhs}')

The simply-typed lambda calculus with inference is powerful, but it cannot express polymorphism — functions that work on any type, like id x = x (identity) or length (works on lists of any element type). Hindley–Milner (HM) type inference extends the system with parametric polymorphism via let-generalization.

The key idea — generalization: After inferring the type of a let-bound expression e₁, generalize over any type variables that are free in the inferred type but not free in Γ (not constrained by the context). The result is a type scheme:

∀α. α → α

This says: id has type α → α for any α. When id is used, we instantiate the scheme by substituting fresh type variables for the universally quantified ones.

The HM algorithm W (Damas-Milner, 1982):

1. W(Γ, e) returns (S, τ) — a substitution and a type.
2. For let x = e₁ in e₂: a. Run W(Γ, e₁) to get (S₁, τ₁) b. Generalize: σ = gen(S₁(Γ), τ₁) = ∀ā. τ₁ where ā are free in τ₁ but not in S₁(Γ) c. Run W(S₁(Γ), x:σ ⊢ e₂) to get (S₂, τ₂) d. Return (S₂ ∘ S₁, τ₂)

Why not generalize inside lambdas? Let-generalization applies only to let bindings, not to lambda parameters. This is a deliberate restriction that makes HM inference complete and decidable (PTIME). Type inference for System F (full second-order lambda calculus with polymorphism inside lambdas) is undecidable.

Value restriction (OCaml/SML): For references and mutable state, unrestricted let-generalization is unsound. Languages like OCaml add the value restriction: only syntactic values (not arbitrary expressions) can be generalized. This prevents the soundness issue at the cost of some expressiveness.

-- Haskell example: let polymorphism in action

-- The identity function has type ∀a. a → a
-- Inferred automatically — no annotation needed
identity x = x

-- Used at multiple types in the same program:
test1 = identity (42 :: Int)    -- instantiated to Int → Int
test2 = identity True           -- instantiated to Bool → Bool
test3 = identity "hello"        -- instantiated to String → String

-- Without let-polymorphism (simply-typed lambda calculus),
-- each use of identity would constrain the type variable,
-- and using it at Int and Bool in the same program would
-- cause a unification failure (Int ≠ Bool).

-- The key: 'identity' is let-bound at the top level,
-- so its type is generalized to ∀a. a → a before use.

Not all type systems are based on equality. Subtyping adds a partial order τ ≤ σ (read: τ is a subtype of σ) meaning that any value of type τ can be used wherever a value of type σ is expected — safely.

The subsumption rule:

  Γ ⊢ e : τ    τ ≤ σ
────────────────────── [SUB]
      Γ ⊢ e : σ

Record/struct subtyping (width and depth):

• Width subtyping: {x:Int, y:Bool} ≤ {x:Int} — a record with more fields is a subtype of one with fewer (you can safely ignore extra fields)
• Depth subtyping: if σᵢ ≤ τᵢ for each field, then {fᵢ:σᵢ} ≤ {fᵢ:τᵢ}

Function type variance: For function types, subtyping is contravariant in the argument and covariant in the result:

  σ₁ ≤ τ₁    τ₂ ≤ σ₂
────────────────────────── [FUN-SUB]
  τ₁ → τ₂ ≤ σ₁ → σ₂

This is the formal version of the Liskov Substitution Principle (LSP): a function that accepts a wider input type and produces a narrower output type is a safe replacement. Intuitively: the caller can give less, and can rely on getting more.

Nominal vs structural subtyping:

• Nominal (Java, C++): τ ≤ σ only if explicitly declared (via extends/implements)
• Structural (TypeScript, OCaml records): τ ≤ σ if the structure of τ is compatible with σ regardless of names

Subtyping and inference: Adding subtyping to HM breaks principal types and makes inference undecidable in general. Languages like TypeScript use bidirectional checking and local subtype inference as pragmatic approximations.

// TypeScript — structural subtyping in action
interface Animal { name: string; }
interface Dog    { name: string; breed: string; }

// Dog is a structural subtype of Animal (it has all required fields)
function greet(a: Animal): string {
  return `Hello, ${a.name}`;
}

const d: Dog = { name: "Rex", breed: "Labrador" };
greet(d);  // OK — Dog ≤ Animal (width subtyping)

// Function type variance:
// (Dog → void) is NOT a subtype of (Animal → void)
// because a function expecting Dog cannot safely accept any Animal
type AnimalHandler = (a: Animal) => void;
type DogHandler    = (d: Dog)    => void;

// Contravariance: AnimalHandler ≤ DogHandler
// (An AnimalHandler can handle any Dog, since Dog ≤ Animal)
const handler: AnimalHandler = (a) => console.log(a.name);
const dogHandler: DogHandler = handler; // OK in TS with strictFunctionTypes

A type checker that only says "type error on line 42" is not useful. Good error messages are one of the hardest engineering challenges in compiler design, and a major area of active research (GHC's error messages have been improving for decades).

Principles of good error messages:

1. Location accuracy: point to the site where the type mismatch makes sense to the programmer, not just where the compiler first detected the conflict. Unification can delay error detection far from the source.
2. Expected vs. actual: always report both what was expected (from context) and what was found (from the expression). "Expected Int, got Bool" is far more useful than "type mismatch".
3. Blame assignment: in inference-based systems, a unification failure can involve two distant constraints. Tracking why each constraint was generated (source location + rule name) lets you blame both sides.
4. Cascading errors: one mistake can trigger a flood of follow-on errors. Heuristics: after a type error, assign a special Error type to the offending expression and continue checking, treating Error as compatible with any type — this suppresses spurious cascades.
5. Context messages: "In the expression x + y:" before the specific error localizes it for the programmer.

Error recovery in practice: Production compilers (clang, rustc) use several strategies:

• Error types: a synthetic ⊥ type that unifies with anything
• Best-effort inference: continue collecting constraints even after a failure
• Suggestions: "did you mean Int instead of Int64?" using edit-distance on type names
• Notes: GHC and rustc attach explanatory notes and sometimes corrected code snippets

Tracking source locations: Every AST node should carry a source span (file, start line/col, end line/col). This span propagates with constraints so that when unification fails, the error can be reported at the correct source location.

# Error reporting with source spans
from dataclasses import dataclass

@dataclass
class Span:
    file: str; line: int; col: int

@dataclass
class TypeError(Exception):
    span: Span
    expected: str
    actual: str
    context: str = ""

    def __str__(self):
        return (
            f"{self.span.file}:{self.span.line}:{self.span.col}: "
            f"Type error{' in ' + self.context if self.context else ''}\n"
            f"  Expected: {self.expected}\n"
            f"  Actual:   {self.actual}"
        )

# Usage in type checker:
def check_add(env, node):
    t1 = typecheck(env, node.left)
    t2 = typecheck(env, node.right)
    if t1 != 'Int':
        raise TypeError(
            span=node.left.span,
            expected='Int',
            actual=t1,
            context='left operand of (+)'
        )
    if t2 != 'Int':
        raise TypeError(
            span=node.right.span,
            expected='Int',
            actual=t2,
            context='right operand of (+)'
        )
    return 'Int'

Bidirectional type checking is a pragmatic middle ground between fully annotated checking and fully inferred HM, and it is the approach used in many modern languages (Kotlin, Scala 3, recent versions of TypeScript, Swift).

Two modes:

• Synthesis (↑): Γ ⊢ e ↑ τ — synthesize the type of e from scratch (like our earlier typecheck function). Used when the type can be determined from the expression alone.
• Checking (↓): Γ ⊢ e ↓ τ — check that e has the given type τ (which comes from context). Used when an expected type is available.

The key rules:

-- Checking a lambda against a known function type:
  Γ, x:τ₁ ⊢ e ↓ τ₂
──────────────────────────── [CHECK-LAM]
  Γ ⊢ λx.e ↓ τ₁ → τ₂

-- Switch from checking to synthesis (subsumption):
  Γ ⊢ e ↑ τ'    τ' = τ
─────────────────────────── [CHK-INF]
      Γ ⊢ e ↓ τ

Why bidirectional? Checking mode propagates type expectations downward — so (λx. x + 1) : Int → Int can type-check the lambda without needing to generate and solve constraints. Synthesis mode propagates types upward from leaves. The combination avoids the global constraint-solving of HM while still inferring many types automatically.

Practical advantage: Bidirectional checking gives much better error messages than HM in languages with complex types (generics, GADTs), because errors are reported locally at the site of the type annotation rather than at a distant unification failure.

-- Bidirectional checking in pseudocode

function synth(Γ, e) -> τ:
    case e of
      Lit n      -> Int
      Var x      -> Γ(x)
      e₁ + e₂   -> check(Γ, e₁, Int); check(Γ, e₂, Int); Int
      e : τ      -> check(Γ, e, τ); τ   -- type annotation
      App(f, a)  -> τ₁→τ₂ = synth(Γ, f)
                    check(Γ, a, τ₁)
                    τ₂
      _          -> error "cannot synthesize type; add annotation"

function check(Γ, e, τ) -> ():
    case (e, τ) of
      (Lam(x,body), τ₁→τ₂) ->
          check(Γ, x:τ₁, body, τ₂)   -- CHECK-LAM
      (If(c,t,f), τ) ->
          check(Γ, c, Bool)
          check(Γ, t, τ)
          check(Γ, f, τ)
      _ ->
          τ' = synth(Γ, e)
          unless τ' == τ:
              error "expected τ, got τ'"   -- CHK-INF