advancedTypes

How does type inference work, and where does it stop working?

Whether the candidate can describe inference as constraint generation plus solving rather than as guessing, and whether they know the specific features that break complete inference. Naming the occurs check is a strong signal; naming why subtyping complicates inference is stronger.

What a strong answer covers

  • The standard algorithm walks the program generating fresh type variables and constraints — this application requires the function type to equal a fresh arrow type, this branch requires both arms to have the same type — and then solves the constraint set by unification. Unification either produces a substitution mapping variables to types or fails, and failure is the type error. Generalization at let-bindings is what makes a polymorphic function reusable at several types.
  • Two things go wrong routinely. The occurs check: unifying a with a -> b would build an infinite type, so the algorithm must refuse it, and that refusal is what turns a self-application into an error message rather than a hang. And unification failure produces the error at the point where two constraints met, which is often far from the line the human considers wrong — the reason inference error messages have a bad reputation.
  • Where complete inference stops: subtyping, because unification wants equality and subtyping wants a direction, so you need constraint solving over inequalities instead. Higher-rank polymorphism, where inference is undecidable and annotation is required. Overloading and type classes, which need a resolution step that can be ambiguous. Mutable references, which need the value restriction or an equivalent to stay sound. And any system with dependent or refinement types.
  • Practical systems therefore infer locally and require annotation at boundaries. Rust and Go infer inside a function body and demand signatures. TypeScript infers aggressively and admits it is not complete. Full Hindley-Milner is the exception, not the norm, and it is the exception in languages without subtyping — which is not an accident.
✓ Green flags
  • Separates constraint generation from constraint solving.
  • Names unification and describes what it produces on success and on failure.
  • Names the occurs check and can give the program that needs it.
  • Explains why subtyping breaks it, in terms of equality versus direction.
  • Knows why local inference plus mandatory signatures is the mainstream compromise, including the API-stability argument.
✗ Red flags
  • "The compiler looks at the value you assign and uses that type." That is the easy case; it says nothing about a function used before it is defined, or a variable constrained by three uses in different branches.
  • "Inference always finds the most general type." Only in systems where principal types exist. With subtyping or overloading there may be no single most general type.
  • "Type inference makes annotations unnecessary." Annotations are also documentation and API boundaries; a fully inferred public signature changes silently when the body changes.
  • "It is just constraint solving, so error messages are a UI problem." Error quality is limited by the algorithm: unification loses the order constraints arrived in, which is the information a good message needs.

Follow-up

Give me a program the occurs check rejects, and say what would happen without it. Then: why do most languages refuse to infer public function signatures?

Implementation challenge

What to ask them to write or trace on a whiteboard.

Infer the type of fun f -> fun x -> f (f x) by hand: write out the fresh variables, the constraints, the unification steps and the final generalized type.

The lessons behind it

Type Inference: Leaving the Type Off →Hindley–Milner: Inference Without a Single Annotation →Unification, and Why `T = List<T>` Must Fail →Parametric Polymorphism and the Theorems You Get Free →The Type Environment: What Γ Is, and Where the Compiler Keeps It →Typing Rules: Reading the Notation With the Line Through It →
← All questions