How the type checking proof avoids the halting problem is by lumping together &quot;ill-formed&quot; and &quot;undecided&quot; into one category: reject the program. Programs which cannot be shown <i>not</i> to be free a type inconsistency are rejected alongside those which are confirmed to have one.<p>(Actually before we even get to that, the type system has to be powerful enough to invoke the problem (i.e. be Turing complete: capable of expressing partial recursive functions).)