Bidirectional Checking: When a Type Is Synthesized and When It Is Checked

The inference machinery of Bottom-Up Expression Typing with Inference Variables treats typing as a single judgment: given an expression, produce a type, unifying metavariables as needed. That judgment is not total. A lambda with unannotated parameters has no type to produce until something tells it what its parameters are, and an empty collection literal has an element type that nothing inside it determines. Bidirectional checking splits the judgment in two so that the direction of information flow becomes explicit in the algorithm rather than emerging from a solver.

Two judgments instead of one

The split is between synthesis and checking. Synthesis, written Γ ⊢ e ⇒ T, takes an expression and produces its type. Checking, written Γ ⊢ e ⇐ T, takes an expression and a type and verifies that the expression has that type, without necessarily computing a type of its own.

Every rule in a bidirectional system belongs to one of the two judgments, and the design work is deciding which. The general pattern is that introduction forms — lambdas, literals, empty collections, null, record literals — check rather than synthesize, because their internal structure is determined by the expected type. Elimination forms — applications, projections, dereferences, conditionals whose branches synthesize — synthesize, because their type is determined by their parts.

The bridge between the judgments is a rule called subsumption, or in its simplest form a change-of-direction rule: if e synthesizes T, then e checks against U whenever T and U are equal, or T is a subtype of U. Without that rule the two judgments are disconnected and nothing typed by synthesis could be used where a check was required. In systems with subtyping the rule carries the subtyping relation; in systems without it, the rule is equality.

Where the direction has to flip

The interesting rules are the ones that switch direction mid-derivation, and there are three that appear in every practical system.

Lambda checking is the first. To check λx. body against A → B, bind x at type A and check body against B. The parameter annotation is not needed because the expected type supplies it. A lambda in synthesis position has nothing to work from and must either be annotated or rejected, which is why Java requires a target type for a lambda expression and why var f = x -> x; is rejected while Function<Integer, Integer> f = x -> x; is accepted.

Application synthesis is the second, and it is where bidirectional systems do the most work. To synthesize the type of f a, synthesize f’s type, decompose it into a function type, and then check a against the parameter type. The argument is checked, not synthesized, which is what lets f (λx. x + 1) typecheck when f’s parameter type supplies x’s type. If f is itself a metavariable — an unannotated parameter used as a function — the system needs a rule to invent a function type with fresh metavariables, which is the point where bidirectional checking starts to need unification again.

The conditional is the third and the most commonly mishandled. if c then a else b can synthesize when both branches synthesize to the same type. It can check when the expected type is known, by checking both branches against it. A system that only implements the synthesizing rule rejects if c then [] else [1] where the expected type is List<Int>, because the then-branch has no type to synthesize; a system that only implements the checking rule rejects if c then a else b in a position where no expected type is available. Practical systems implement both, and the choice between them is driven by whether the surrounding context is checking or synthesizing.

What the split buys

The gain is that the algorithm never has to solve a constraint whose solution is not determined by local information. Every metavariable introduced during checking is either solved immediately by the expected type or reported as an error, and the constraint set never grows to span a whole module. That is what makes error messages localizable: a failure in a checking judgment can name the expected type and the actual type at the node where they disagree, rather than reporting that some constraint from elsewhere in the program could not be satisfied.

The second gain is that annotations become meaningful. In a fully inferring system an annotation is a hint; in a bidirectional system it is a boundary where synthesis stops and checking begins, and the checker can rely on it. A function signature is checked against the body, not unified with it, so the body is checked against a known type and the error messages point into the body.

The third gain is predictable performance. Checking a lambda against a known type is linear in the size of the lambda. Synthesizing a type for the same lambda requires inventing metavariables for each parameter and solving them, and the cost of that solving grows with the program: unification-based inference over a whole module has no linear-time guarantee, and it does not degrade gracefully when a single missing annotation forces the checker to infer a type parameter that the rest of the code never constrains.

What it costs

Completeness is the price. A bidirectional system rejects programs that have a unique most general type but no annotation to drive the checking. The canonical example is the unannotated identity function passed to an unannotated higher-order function: nothing in the syntax supplies the parameter type, and the system reports an error rather than inferring.

Systems mitigate this by adding a limited form of inference at specific points. Local type inference allows metavariables in argument positions when the function’s type is known, which covers most real code without opening the door to global solving. Java’s diamond operator does the same for constructor type arguments: the target type of the assignment or the declared type of the variable supplies the argument, and the diamond is an error where no such context exists, as in the statement new ArrayList<>();.

The second cost is that the split must be maintained consistently. A rule that synthesizes in one place and checks in another, without a documented change-of-direction rule, produces a system whose behavior depends on traversal order. The classic symptom is that a program typechecks when the expression is written one way and fails when it is written another way that is semantically identical, because one form reaches a synthesizing rule and the other a checking rule.

The third cost is the interaction with overloading. A syntactic form whose type depends on which overload is chosen cannot be typed without knowing that choice, and the choice depends on the argument types, so the two decisions are entangled. Java resolves this with poly expressions: a method invocation or a lambda is poly-expressive when its arguments are, and in that case the target type propagates inward through the argument expressions instead of being computed bottom-up. A system without an equivalent rule must synthesize each argument first and loses the cases where the argument’s own type is only determined by the parameter’s.

A minimal implementation

The skeleton below shows the two judgments for a small expression language in OCaml, with function types and a unit type. The check function recurses into synth at the change-of-direction rule.

type ty = TUnit | TArrow of ty * ty

exception TypeError of string

let rec equal a b =
  match a, b with
  | TUnit, TUnit -> true
  | TArrow (p1, r1), TArrow (p2, r2) -> equal p1 p2 && equal r1 r2
  | _ -> false

let rec synth ctx e =
  match e with
  | Var x -> List.assoc x ctx
  | Lam _ -> raise (TypeError "lambda needs an expected type")
  | App (f, a) ->
      (match synth ctx f with
       | TArrow (p, r) -> check ctx a p; r
       | _ -> raise (TypeError "application of a non-function"))
  | Unit -> TUnit

and check ctx e expected =
  match e, expected with
  | Lam (x, body), TArrow (p, r) ->
      check ((x, p) :: ctx) body r
  | _ ->
      let actual = synth ctx e in
      if not (equal actual expected) then
        raise (TypeError "type mismatch")

The Lam case in check is the whole idea: the expected type decomposes into a parameter type and a result type, the parameter is bound at the known type, and the body is checked against the result. The fallback case is subsumption: synthesize, then compare.

The snippet omits metavariables, which a real system needs for partially known types. Once they are present, the equality test in the change-of-direction case must compare representatives and must not unify; a checking comparison that unified would silently accept mismatches by binding a metavariable to whatever it compared against, which is the failure mode described next.

Where a bidirectional checker goes wrong

The most damaging bug in a bidirectional checker is a check that unifies instead of comparing. When the expected type contains a metavariable — which happens whenever checking occurs under a partially solved context — unification binds the metavariable to the actual type, and the comparison always succeeds. The result is a checker that accepts ill-typed programs in exactly the cases where inference was incomplete, which is the hardest class of bug to notice because well-annotated programs still fail correctly.

The second is direction leakage in recursive calls. A rule that checks a subexpression but then uses its synthesized type for something else — a match arm that checks against the scrutinee’s type but also records the arm’s own type for later use — needs the synthesized type to be the expected one. If the check succeeded via a subtyping rule, the arm’s actual type may be a subtype, and using the expected type in its place loses information that a later pass needs.

The third is error attribution. A checking failure deep inside a lambda reports a mismatch between two types that the user never wrote, because both came from the expected type. Diagnostics need to distinguish “the expression’s type does not match the expected type” from “the expression cannot be checked at all”, and the second is often the more actionable message because it points at a missing annotation. Producing that message requires the checker to know which rule failed, not just that some comparison failed — a reason that Error Types and Recovery in a Type Checker has to preserve through the recovery path.

The fourth is the boundary with generalization. A bidirectional system that also generalizes let-bound definitions must decide whether generalization happens at synthesis or at checking, and the answer changes which programs are accepted. That decision is the subject of Let-Polymorphism and Where Generalization Happens.