Bottom-Up Expression Typing with Inference Variables

A checker that requires every expression to have a type before its parent can be checked works only for languages where every subexpression carries an annotation. The moment a lambda appears without parameter types, or an empty collection literal appears without an element type, the child’s type is not known when the parent is visited. Bottom-up checking handles this by giving the child a placeholder — an inference variable — and recording a constraint that must hold, to be solved when enough information arrives.

The shape of the walk

The checker is a recursive function from expression node to type. For a literal, the type is immediate: an integer literal has the type of its default integer type unless context says otherwise, a string literal has the string type. For a variable, the type is read from the resolved binding. For an operator or a call, the children are checked first, their types are combined into a requirement, and the result type is produced from the operator’s signature.

The difficulty is entirely in “combined into a requirement”. If both children have concrete types, the requirement is a check: does the operator accept them, and if so, what does it return. If one child has an inference variable, the requirement becomes a constraint to be solved later rather than a decision made now.

The result type can itself be an inference variable. An empty list literal has type List<α> for a fresh variable α; a call to a generic function with no annotated arguments returns β where β is a fresh variable. Both are legitimate: the expression has a type, it is just not yet determined.

Metavariables as union-find nodes

The standard representation for an inference variable is a node in a union-find structure. Two operations matter: fresh() creates a new unbound node, and unify(a, b) merges two nodes, recording that their types must be equal. A bound node holds a type constructor and its arguments, which may themselves be metavariables.

A union-find forest alone is not enough, because unification is not just an equivalence relation over variables: a variable may be bound to a compound type whose arguments are themselves variables, as in α = List<β>. The usual representation is a mutable cell per metavariable that starts unbound and later holds a link to a type, with find following links to the representative and compressing the path. If α links to List<β> and β links to Int, then repr(α) is List<Int> after two hops and one on every later lookup. Representing the same relation with a substitution map keyed by variable would require composing substitutions on every lookup, which is O(n) in the depth of the chain; path compression on the links makes the lookup nearly constant amortized. Union-find appears where two variables must be identified with no structure between them, as when an argument position has type α and the parameter has type β.

Two details matter for correctness. First, unification must follow bindings on both sides: unifying a metavariable with a concrete type binds it, but unifying two metavariables that are already in the same equivalence class is a no-op rather than a re-binding. Second, a metavariable must never be bound to a type that contains itself. That is the occurs check.

Why the occurs check is not optional

Without the occurs check, unifying α with List<α> succeeds and produces a cyclic type. Every later operation that walks the type — printing it in a diagnostic, computing its size, generating code — diverges. The check walks the type being bound, looking for the metavariable’s representative, and fails the unification if it appears.

The cost is a traversal of the type on every binding, which for a deeply nested type is proportional to its size. Implementations that care about the constant use a union-find with a size or rank field and a traversal budget, or record the set of free metavariables of each type as it is constructed so the check is a set membership test. The naive traversal is fine for a first implementation and is what most textbooks show.

The occurs check also catches a class of real programmer errors: a recursive function whose type would have to be infinite. The error message is poor if it reports only “cannot construct infinite type”; naming the two expressions that forced the cycle is what makes the diagnostic usable.

Constraints as deferred work

A checker that unifies at every node, as soon as the node is visited, breaks when a node’s type depends on information that has not arrived yet. Checking a lambda passed to a higher-order function works because the callee’s signature is known by the time the argument is visited, so the parameter type is available. The case that defeats the eager scheme is an expression whose type constrains a node visited earlier, as when a generic call’s result type is fixed by a later assignment, or an overloaded operator whose result depends on operand types in a way that no single unification expresses.

The usual design records constraints and solves them after the walk. A constraint is a pair of types with a relation — equality, subtype, or “this call’s arguments must satisfy this signature” — and the solver processes them in an order that resolves dependencies. Equality constraints are unification and can be processed eagerly; subtype constraints are not symmetric and must be deferred until the subtyped side is known.

Deferring everything has a cost: the constraint set grows with expression size, and a solver that processes constraints in arbitrary order can be quadratic in the worst case. Processing equality constraints eagerly and deferring only the asymmetric ones keeps the set small in practice, because most of a program’s type structure is equality-shaped.

Where inference must stop

Full inference without annotations is undecidable in general for languages with subtyping and polymorphic recursion, and even where decidable it produces types the programmer did not intend. Every practical language draws a line.

Java draws it at lambda parameters: a lambda without parameter types is checked only in a context that supplies a target type, and the target type comes from the surrounding assignment, invocation, or cast. That is local type inference, and it is deliberately not a global constraint solver: the target type propagates inward from the context, and a lambda whose parameter types cannot be determined from the context is an error rather than a deferred constraint.

Go draws it at composite literals and generic calls: the element type of an empty composite literal comes from the assignment context, and a call to a generic function infers type arguments from the argument types by unification, failing if a type parameter appears only in the result. The failure rule is important: func New[T any]() *T cannot be called without explicit type arguments, because nothing constrains T. A checker that silently picked an arbitrary type would compile programs whose meaning depends on an implementation detail.

Haskell draws it much further out, inferring principal types for whole modules by solving constraints over the entire program. The price is that the inferred type is not always the type the programmer had in mind, and that type errors surface where the constraint finally fails, which can be far from the expression that introduced the mismatched type. Desugaring obscures that path further: a class constraint in the source is inferred at the use of an overloaded name, and the reported site can be inside a do block long after the binding that made the type wrong.

What the walk returns besides a type

A checker that returns only a type from each expression node throws away information that the same traversal already computed and that later passes need. Four properties are worth threading through the return value, because recomputing them requires a second walk over the same tree.

The first is whether the expression denotes a storage location rather than a value. An assignment’s left side must be a place: a variable, a field access, an array element, a dereference. A call result is not a place in most languages, and the difference is not visible in the type — an int variable and an int-returning call both have type int. Carrying a place flag on the node lets the assignment rule reject f() = 3 without a special case in the assignment code that re-inspects the node’s syntax.

The second is mutability, which in languages with const or final is a property of the binding, not of the type. A const-qualified binding yields an expression whose type is the same but which cannot appear on the left of an assignment. Since the flag lives on the binding record produced by name resolution, the checker reads it there and propagates it through field accesses: a field of a const struct is itself const in C, which is a rule about the propagation, not about the field’s declaration.

The third is constant-ness in the compile-time sense. An initializer for an enumeration value, an array bound, or a case label must be a constant expression, which in C means it can be evaluated by the compiler without knowing any run-time values. That is a property of the expression tree, not of its type: 2 + 3 and x + 3 share a type and differ in constant-ness. The check is easiest during the same bottom-up walk, since a node is constant exactly when its children are and its operator is constant-foldable.

The fourth is the value category needed for overload resolution. Choosing between a move and a copy constructor, or between an lvalue and rvalue overload of a method, requires the category to be known at the call site, and it is determined by the same rules that determine place-ness. Computing it once and storing it avoids the situation where two passes disagree about whether an expression is an lvalue, which is a class of bug that produces silently wrong overload choices.

A small unifier

The code below is a complete unifier for a first-order type language with variables, written in OCaml. It is the core that every inference-based checker shares.

type ty =
  | TVar of tvar ref
  | TCon of string * ty list

and tvar = Unbound of int | Link of ty

let counter = ref 0

let fresh () = incr counter; TVar (ref (Unbound !counter))

let rec repr t =
  match t with
  | TVar ({ contents = Link t' } as r) ->
      let t'' = repr t' in
      r := Link t'';      (* path compression *)
      t''
  | _ -> t

exception Unify of string

let rec occurs v t =
  match repr t with
  | TVar r -> r == v
  | TCon (_, args) -> List.exists (occurs v) args

let rec unify a b =
  match repr a, repr b with
  | TVar ra, TVar rb when ra == rb -> ()
  | TVar ra, t ->
      if occurs ra t then raise (Unify "infinite type");
      ra := Link t
  | t, TVar rb ->
      if occurs rb t then raise (Unify "infinite type");
      rb := Link t
  | TCon (n1, a1), TCon (n2, a2) ->
      if n1 <> n2 || List.length a1 <> List.length a2 then
        raise (Unify (Printf.sprintf "%s vs %s" n1 n2));
      List.iter2 unify a1 a2

The repr function is what makes the structure work: it follows links to the representative and compresses the path on the way back, so a chain of bindings collapses to one hop after the first lookup.

When the unifier misbehaves

The unifier above is first-order: it unifies types with types, never a type with a type scheme. Unifying a polymorphic type with a monotype requires instantiation first — replacing the scheme’s bound variables with fresh metavariables — and forgetting that step produces the error where two uses of an identity function are forced to share one type.

Rigid variables are the second trap. A type parameter inside a generic function’s body is not a metavariable; it must not be unified with an arbitrary type. A checker that represents both with the same union-find node will accept a function body that treats its type parameter as Int, which is unsound. The representation needs a distinct constructor for skolems, and unification must refuse to bind them.

The third is the interaction with error recovery. A unification failure that raises an exception aborts the whole expression’s checking, losing every subsequent diagnostic in the subtree. Recording the failure, binding the node to an error type, and continuing produces better output at the cost of needing every rule to tolerate the error type. The design of that tolerance is in Error Types and Recovery in a Type Checker.

Finally, generalization. A metavariable that remains unbound at the end of a declaration’s checking is either a genuine inference result to be generalized or a hole that will be filled by a later use. Deciding which requires knowing the scope of the variable, which is why let-polymorphism is a separate mechanism rather than a detail of the unifier.