A type checker earns trust through its errors, and this one has exactly three kinds, each built earlier in the project. An unbound variable is a name used out of scope, from the very first environment lesson. A type mismatch is unification refusing to make two types equal - a non-Bool condition, an argument of the wrong type, disagreeing branches - and it accounts for nearly every error a real program hits. An infinite type is the occurs check firing on a self-referential term like \x. x x. Today confirms all three travel through Report and pick up a source position from their enclosing At, so the programmer always gets what went wrong and where.

There is one honest limitation worth naming, because it shapes how the capstone behaves: this checker reports the first error it meets and stops. The moment a unification fails, inference returns that error and unwinds - it does not recover and keep going to collect every mistake in the program at once, the way a production compiler does with error recovery. That is a deliberate scope line for a teaching-grade checker, and a natural thing to note in the caveats and to try as an extension. With the diagnostics complete, everything is in place for the capstone: one program inferred to its principal type, one reported at its error.