The only way the type-checker is by finding unbound variables, or by
unification errors. The former cannot occur with closed terms. In turn,
unification can failed either with occur check or with clashes when
attempting to unify two terms with different top symbols. Recursive types
removes occur-check. In the absence of primitive operations, types are
either variables or arrow types. The only type constructor is →, so
that there will never be any clash during unification.