Bidirectional Type Checking and Where Annotations Flow

Unification-based inference works because every construct generates constraints of the same shape. That uniformity disappears as soon as a language has constructs whose type cannot be determined from their parts: a lambda with no annotation, a literal whose type is overloaded, an empty collection, a pattern match with no scrutinee type. Bidirectional checking handles these by splitting the single judgment into two, one that infers a type and one that checks a term against a type supplied by context, and by specifying exactly when control passes from one to the other.

Two judgments, not one

The inference judgment Γ ⊢ e ⇒ τ produces a type. The checking judgment Γ ⊢ e ⇐ τ consumes one. The two are related by a subsumption rule: anything that can be inferred can be checked, by inferring a type τ' and then confirming that τ' and the expected type τ agree — equal in the simply typed case, related by subtyping or by an instantiation of τ' once the language has either.

The direction that is not free is the reverse. Checking a term against a type does not produce a type the rest of the program can use, so a construct that only has a checking rule must appear in a position where the expected type is known. That is the whole source of the annotation burden in bidirectional systems, and the design work is in arranging the rules so that the burden falls where the programmer expects it.

The gain is precision. A checking rule can propagate the expected type into subterms, which lets a lambda’s parameter type be known without an annotation and lets an empty list literal take its element type from context. The comparison with the pure inference algorithm is direct: the rule for a lambda in unification-based inference must invent a fresh variable for the parameter and unify it later, while the checking rule is simply that λx. e checks against τ₁ → τ₂ whenever e checks against τ₂ under the environment extended with x : τ₁.

The checking rule is simpler, requires no fresh variables, and fails immediately and locally when the shapes do not match.

Where the switch happens

Every bidirectional system specifies a set of change points where the direction flips. The standard arrangement, as presented by Dunfield and Krishnaswami, is:

• Variables and constants are inferred.
• Application infers its function, then checks the argument against the function’s domain.
• A lambda checks when the expected type is a function type, and otherwise infers only if its parameter is annotated.
• Ascription always infers, and its result is checked against the ascribed type.
• let infers the right-hand side and checks the body under the extended environment.
• Conditionals check when the expected type is known, and infer by finding a common type otherwise.

The last one is the interesting case. if c then e₁ else e₂ under an expected type τ simply checks both branches against τ. With no expected type, the checker must infer both branches and join their types, which requires a join operation on the type lattice. If the lattice has no least upper bound for some pair — two record types with different fields, say — the expression is rejected even though it would be accepted in a context that supplies a type. This is why an annotation on a conditional’s result sometimes fixes an error that looks unrelated.

The application rule deserves a note. Inferring the function and checking the argument is one convention, not the only one: a typical ML-family checker infers both the function and the argument and unifies the function’s domain with the argument’s type, so an unannotated lambda argument is checked against a fresh variable and fails on its parameter type rather than never being checked at all. The bidirectional rule instead requires the function’s type before the argument can be checked, which is what lets the argument take its type from context, and is what fails when the function’s type is itself not yet known. The choice is a design decision with no universally correct answer, and it is why error messages in different ML-family languages point at different subterms for the same mistake.

Checking patterns and the annotation it saves

Pattern matching is where bidirectional checking earns its keep. A match on a scrutinee of known type can check each pattern against that type, which propagates constructor argument types into the pattern variables. Without that, every pattern variable would need a fresh unification variable and the constraints would multiply.

# Sketch of a checking rule for a constructor pattern
# match e with P1 -> b1 | P2 -> b2, expected type T
def check_match(env, scrutinee, arms, expected):
    scrut_ty = infer(env, scrutinee)
    for pat, body in arms:
        env2 = check_pattern(env, pat, scrut_ty)   # binds variables, no fresh vars
        check(env2, body, expected)                # branches share the expected type

check_pattern walks the pattern and the scrutinee type together. A constructor pattern requires the scrutinee type to be that constructor applied to arguments, and binds each pattern variable to the corresponding argument type. There is no inference step, so a pattern that does not match the scrutinee’s shape is an immediate error at the pattern’s location rather than a constraint failure reported later. The work done per pattern is proportional to the pattern’s depth and to the number of variables it binds, with no fresh variables allocated, so a match with n arms of depth d costs O(nd) type comparisons in place of unification steps.

The same mechanism extends to GADT-style refinement: when a constructor’s return type is more specific than the scrutinee’s type — an index fixed to a particular type rather than left as a parameter — the pattern match refines the environment for that branch, and the type checker records that the branch is only reachable under the equalities the constructor’s return type imposes. The refinement is a substitution on type variables, applied to the branch’s environment and expected type. This is where bidirectional checking stops being a convenience and becomes necessary: the refinement cannot be expressed as a unification constraint on the outer type, because the constructor’s return type must be unified with the instantiated scrutinee type rather than constrain it, and it is a local assumption that must not escape the branch.

Elaboration is the real output

A practical checker does not just accept or reject. It produces a core term in which every implicit argument, coercion, and dictionary is explicit. The bidirectional structure makes this natural: the checking judgment returns the elaborated term, and the expected type is available exactly where the elaborator needs it to decide what to insert.

For a lambda checked against τ₁ → τ₂, the elaborator emits a lambda whose parameter carries the annotation τ₁, because the core language requires it. For an application of a polymorphic function, the elaborator emits the type arguments that were inferred, so the core term is monomorphic. For an empty collection checked against List τ, the elaborator emits the element type.

This is why the choice of change points is not cosmetic. Each one determines where the elaborator has enough information to insert the implicit pieces, and moving a change point changes which programs elaborate without annotations. A system that infers an application’s function and checks its argument can insert the function’s type arguments at the application node; a system that does the reverse must defer them.

The failure modes

Propagation stops at the wrong place. If a checking rule does not propagate the expected type into a subterm, that subterm must be inferred, and the annotation burden reappears one level deeper. The classic example is a checking rule for a record literal that checks each field’s expression against the field’s declared type, versus one that infers each field and compares. The first admits programs the second rejects — a field expression that needs its expected type, such as a bare lambda — so a system that does the second has a bug in its rule design rather than a fundamental limit.

Joins are not principal. As noted, inferring a conditional requires a join, and a join may not exist. Systems that avoid the problem by requiring annotations at conditionals have traded expressiveness for determinism.

Errors are directional. A checking failure reports “this term does not have the expected type”, which is useful when the expected type came from an annotation but unhelpful when it came from a distant inference. A common mitigation is to record the provenance of each expected type — the syntax node that produced it — so the message can say where the expectation originated.

Subtyping complicates the switch. With subtyping, the rule relating the judgments becomes Γ ⊢ e ⇒ τ' and τ' <: τ, not equality. The subtype check may be deferred if either side contains variables, so the checking judgment can succeed with a pending constraint. This is the mechanism by which structural subtyping and bidirectional checking coexist, and it means the elaborator may insert a coercion that was not visible in the source.

Why not just infer everything

Full inference for a language with lambdas, overloading, records, and subtyping is well past what a unification solver can do: the combination is undecidable in general, and the fragments where it is decidable produce types that are hard to explain. Bidirectional checking is a deliberate retreat: it gives up the guarantee of inferring a type for every typable term in exchange for a deterministic, local algorithm whose failures point at the construct that needed help.

The exchange is visible in the language’s surface. A bidirectional language typically requires annotations on top-level definitions, on lambda parameters in some positions, and on terms whose type would otherwise be ambiguous. In return, it can support features that unification cannot: implicit arguments resolved by type, overloaded literals, refinement types checked against a solver, and dependent types where the expected type drives the checking of the term. Each of those is a place where the type must be known before the term is examined, and each is only expressible because the judgment was split in two. The most demanding instance of that pattern is refinement type checking, where the expected type is not just propagated but proved.