Error Types and Recovery in a Type Checker

A checker that stops at the first error is trivial to write and useless in practice. A checker that continues must answer a question the first design never faces: what type does a subexpression have when its type could not be computed? The answer determines whether subsequent errors are real or artifacts, and getting it wrong produces a compiler whose diagnostics get worse the more errors a program contains.

The failure mode that makes naive continuation wrong

Suppose an expression refers to an undeclared name. Its type is unknown. If the checker aborts the whole expression, the enclosing statement is unchecked and the rest of the function is skipped; one error is reported and everything downstream is silently ignored. If the checker instead assigns the expression some arbitrary type — say, the type of the first operand it can find — the parent expression may then typecheck, and the checker proceeds with a program whose meaning it has fabricated.

The dangerous case is the second. A fabricated type can make a real error disappear: the checker concludes that f(undeclared) matches f’s parameter because it guessed, and the user sees only the undeclared-name error while a genuine mismatch further along goes unreported. It can also make the checker diverge, if the fabricated type is a recursive one that unification then chases.

The correct answer is a distinguished type that is compatible with everything and from which nothing can be concluded. Call it the error type, written ⊥ in the typing rules. It is a top and a bottom at once for the purpose of checking: ⊥ checks against any expected type, and any expression checks against ⊥. That double compatibility is what lets the checker continue without committing.

What the error type must absorb

The rules are few but must be applied consistently, and the consistency is where implementations fail.

Unifying ⊥ with any type succeeds and produces ⊥. If it produced the other type, information would flow from a failure into a success, and a later error could be masked. Unifying two error types succeeds. Unifying a type containing ⊥ as a subcomponent — List<⊥> — with List<Int> must succeed by structural descent and produce List<⊥>, not List<Int>.

Subtyping must treat ⊥ as both a subtype and a supertype of everything, for the same reason. A checker with a subtype relation that puts ⊥ at the bottom only will reject ⊥ in a position requiring a supertype, generating a second error for the first failure. In a system without subtyping, the corresponding rule is that the compatibility test used by the checking judgment accepts ⊥ on either side, without consulting equality.

Overload resolution must treat ⊥ as a poisoned argument: it matches no candidate, but it also must not cause a “no matching overload” error, because the argument’s failure already produced one. The resolution rule is that a call with any ⊥ argument yields ⊥ without reporting. Without that rule, every failed argument generates an additional error, and a single mistake in a large call produces a wall of them.

Member access on ⊥ yields ⊥ without a diagnostic, and so does a call of a ⊥-typed callee. Both are consequences of the same principle: a failure has already been reported somewhere upstream, and re-reporting it at every use is noise.

The principle has a name in the diagnostics literature: errors should be reported at their origin, and propagation should be silent. Applying it uniformly means the checker’s rules are written in two layers — a rule that computes a type, and a guard that short-circuits to ⊥ when any input is ⊥ — and the guard must be present in every rule, not just the common ones.

Recovery granularity

Continuing past an error requires choosing a unit of recovery. Three are common.

Expression-level recovery replaces the failing subexpression with ⊥ and checks the rest of the expression. This gives the finest granularity and the most errors: a function body with ten mistakes reports ten. It also risks reporting errors that depend on the failed subexpression’s type, which is why the guard rules matter.

Statement-level recovery skips the failing statement and continues with the next. It is what a parser does with a synchronizing token, and it is the right granularity when the error is likely to have corrupted the statement’s meaning. The checker must then decide the statement’s effect on the environment: a declaration whose initializer failed still introduces a binding, typed ⊥, so that later uses of the name do not produce undeclared-name errors.

Declaration-level recovery skips the whole declaration and continues with the next top-level item. This is the coarsest and produces the fewest errors, at the cost of hiding genuine errors inside a body that had one unrelated failure.

The choice interacts with the language. A language with heavy inference cannot do expression-level recovery well, because a failed subexpression leaves metavariables unsolved and the solver’s remaining constraints may be unsatisfiable for reasons unrelated to the original error. Such checkers typically recover at the declaration level and mark the declaration’s exported type as ⊥ or as the annotated signature.

Reporting the right number of errors

Every compiler that continues past errors needs a limit, and the limit is a user-experience decision with a technical consequence.

The technical consequence is that error cascades are common and their length is not proportional to the number of real mistakes. A missing import produces an undeclared name at every use of the imported symbol; a wrong type in a widely used function produces a mismatch at every call site. A checker that reports all of them makes the first error, the real one, hard to find among hundreds of consequences.

The common mitigations are deduplication and suppression. Deduplication collapses repeated identical diagnostics — the same message at different sites can be reported once with a count and a list of locations. Suppression is stronger: after reporting an error at a declaration, mark that declaration as poisoned and refuse to report errors that depend on it. Implementing suppression requires the checker to track, for each diagnostic, which prior failures it depended on, which is the provenance information that is also needed for good messages.

A limit of a few dozen errors before the checker stops is typical, with a final message stating that further errors were suppressed. The number is arbitrary; the important property is that the limit exists and that the checker reports it rather than silently truncating.

Preserving enough information to explain the failure

A recovery strategy that discards the failed expression’s structure cannot produce a useful message. The checker should record, at each error node, the type it expected and the type it computed, plus a reason for the mismatch that is more specific than “types differ”.

Three reasons cover most cases and deserve distinct messages. A rigid type variable that was expected but a concrete type was found means the code is trying to specialize a generic; the message should name the type parameter. A metavariable that remained unsolved means inference could not determine a type; the message should say which expression’s type was undetermined and suggest an annotation. An arity mismatch — a function type with two parameters checked against a call with three arguments — should be reported as such rather than as a general mismatch, because the fix is different.

Provenance also matters for the expected type. When the expected type came from an annotation the user wrote, the message can point at it. When it came from an enclosing call, the message should name the call. When it came from unification with another expression, the message should name that expression. Storing a single origin per type — a node identifier and a short description — costs a word per type and turns a mismatch into a two-location error, which is what most modern checkers show.

Interaction with the passes around it

Recovery in the checker is not isolated. The resolver’s failures, described in Resolving Identifier Uses Against a Stack of Lexical Scopes, produce unresolved names that must be bound to something so the checker does not report them again; the convention is a synthetic binding with the error type and a flag marking it, so the checker’s guard rules can recognize it without special-casing by name.

Definite assignment, covered in Definite Assignment as a Flow-Sensitive Dataflow Problem, must treat an error-typed variable as assigned, or a failed declaration produces an unassigned-use error at every subsequent read. The same principle applies to capture analysis: a closure capturing an error-typed variable should not be reported for capturing an uninitialized value.

Downstream of the checker, a ⊥ type must never reach code generation. The usual arrangement is that compilation stops after semantic analysis if any error was reported, so ⊥ exists only inside the front end. A compiler that proceeds to code generation after errors — some do, to report more errors from later passes — must lower ⊥ to a concrete type at the boundary, and the choice of which type is a source of subtle miscompilation. The safe choice is to emit a trap or an unreachable at every ⊥-typed operation, so that a program compiled with errors fails visibly if it is run.

A guard in practice

The shape below is the guard layer in a checker written in Rust, expressed as a small combinator over a result type. The point is that every rule routes through it, so the short-circuit cannot be forgotten.

#[derive(Clone, PartialEq)]
pub enum Ty { Error, Int, Bool, Fun(Box<Ty>, Box<Ty>) }

pub struct Diag { msg: &'static str }

pub struct Checker { errors: Vec<Diag>, limit: usize }

impl Checker {
    fn report(&mut self, msg: &'static str, _got: &Ty, _want: &Ty) {
        self.errors.push(Diag { msg });
    }

    fn compatible(&self, a: &Ty, b: &Ty) -> bool {
        matches!((a, b), (Ty::Error, _) | (_, Ty::Error)) || a == b
    }

    fn guard<F>(&mut self, parts: &[&Ty], f: F) -> Ty
    where F: FnOnce(&mut Self) -> Ty {
        if self.errors.len() >= self.limit { return Ty::Error; }
        if parts.iter().any(|t| matches!(t, Ty::Error)) {
            return Ty::Error;      // upstream failure, stay silent
        }
        f(self)
    }

    fn check_app(&mut self, callee: &Ty, arg: &Ty) -> Ty {
        let fun = match callee {
            Ty::Fun(p, _) if !self.compatible(arg, p) => {
                self.report("argument type mismatch", arg, p);
                return Ty::Error;
            }
            Ty::Fun(_, r) => r,
            _ => {
                self.report("callee is not a function", callee, &Ty::Error);
                return Ty::Error;
            }
        };
        (**fun).clone()
    }
}

Two properties of this shape are worth naming. The limit check happens before any work, so a program with thousands of errors does not pay for checking all of them. And the operand types are borrowed by guard and by check_app, so the caller keeps ownership of both and a rule that needs to inspect them after the guard still can.

The limits of recovery

Recovery cannot make a checker’s answer correct; it can only make its output useful. A program with errors has no type, and the checker’s job is to produce the most informative set of messages, not a type. Systems that build tooling on top of the checker — editors, refactoring engines, language servers — need a type for every expression regardless, which is why they run a recovery-oriented checker that assigns ⊥ liberally and accepts that some results are meaningless.

The failure mode to avoid is a recovery path that changes the meaning of programs that have no errors. A guard that fires too eagerly — treating a metavariable as an error, for instance — silently accepts ill-typed programs in the no-error case, and that is far worse than a verbose diagnostic. The guard’s condition must be exactly “a failure has already been reported here”, and every widening of it needs a test that a well-typed program still produces no diagnostics.