This is what the whole project was for. Hand the checker compose, the function that chains two functions - \f. \g. \x. f (g x) - with no annotations anywhere, and it works out the most general type any implementation could have: (a -> b) -> (c -> a) -> c -> b. Every mechanism you built carries part of that answer. Fresh variables stand in for the unknown types of f, g, and x. Application unifies each call against an arrow to a fresh result. Substitutions thread the discoveries through. Generalization at the let makes compose polymorphic. And Show renames the tangle of internal variables to the clean a, b, c a reader expects. Nobody told the checker any of these types; it derived the principal type from the structure of the code alone.

The second half is the other side of the promise. let x = 5 in if x then 1 else 2 binds x to Int and then uses it as a condition, and the checker refuses - cannot unify Int with Bool at line 1, col 18 - naming both the conflict and the exact spot. From three ground types and an equality check, you have built a real Hindley-Milner type checker: it infers the principal type of an unannotated program across functions, let-polymorphism, recursion, tuples, lists, and records, and it reports the first type error with a source location. It takes a pre-built AST rather than parsing source, and it stops at the first error rather than collecting them all - honest limits for a teaching-grade checker - but the core it implements is exactly the one at the heart of ML, Haskell, and every language that infers your types for you. That is a real type checker, and it is yours.