19. Type Checker: Bidirectional Type Checking

The Type Checker is designed as a standalone, stateless engine. Rather than relying on standard Hindley-Milner (HM) type inference, which uses global unification, this architecture implements Bidirectional Type Checking (based on the models of Pierce & Turner, and Dunfield & Krishnaswami).

The Flaw of Global Unification

Standard inference algorithms like Hindley-Milner solve types by generating constraints across the entire program and unifying them in a massive global pass.

While theoretically powerful, this can create a severe UX problem for developers regarding non-local error reporting. If a type mismatch occurs, the constraint solver often does not realize the system is invalid until it has traversed to a different, unrelated expression. The resulting error messages can be difficult to trace because they are reported far from the actual source of the bug.

The Bidirectional Architecture

Bidirectional Type Checking abandons global unification. Instead, it splits type evaluation into two mutually recursive, localized modes:

1. Synthesis ($\Rightarrow$): The checker looks at an expression and works “bottom-up” to infer its type.
2. Checking ($\Leftarrow$): The checker is given an expected type from the surrounding context and pushes it “top-down” into the expression to verify it.

Synthesis (Bottom-Up)

When the checker encounters a standalone expression with no context, it synthesizes the type from the leaves of the AST up to the root.

// Example: Synthesizing `true`
Type type = synthesize(LiteralBoolNode); 
// Returns: Type::Bool

Checking (Top-Down)

When the checker has contextual type information (like a variable declaration or a function signature), it switches to Checking mode. It pushes that expected type down into the expression.

// Example: `let x: float = 5;`
// The context demands a float. The checker pushes it down.
bool success = check(LiteralIntNode(5), Type::Float);

Instead of synthesizing 5 as an integer and throwing an error because it doesn’t match float, the integer literal node receives the Float expectation from above. The compiler can use this context to accept the expectation (for example, if the language designer chooses to allow an implicit promotion from int to float in checking mode).

Error Localization

Because information flows both ways—expectations down, inferences up—the type checker often knows what it expects at a given AST node.

If a check() fails, the algorithm can halt on the specific AST node that caused the violation. This localized architecture significantly improves error reporting precision, generally pointing the developer closer to the location where the types actually mismatched, rather than reporting the error globally.

Next Module: Borrow Checker