Divergence of Fsub type checking

System F-less than or equal to is an extension of second-order typed lambda calculus, where a subtype hierarchy among types is defined, and bounded second-order lambda abstraction is allowed. This language is a basis for much of the current research on integration of typed functional languages with subtypes and inheritance. An algorithm to perform type checking for F-less than or equal to expressions has been known since the language Fun was defined. The algorithm has been proved complete, by the author acid Curien, which means that it is a semi-decision procedure for the type-checking problem. In this paper we show that this algorithm is not a decision procedure, by exhibiting a term which makes it diverge. This result was the basis of Pierce's proof of undecidability of typing for F-less than or equal to. We study the behavior of the algorithm to show that our diverging judgement is in some sense contained in any judgement which makes the algorithm diverge. On the basis of this result, and of other results in the paper, we claim that the chances that the algorithm will loop while type-checking a ''real program'' are negligible. Hence, the undecidability of F-less than or equal to type-checking should not be considered as a reason to prevent the adoption of F-less than or equal to as a basis For defining programming languages of practical interest. Finally, we show the undecidability of an important subsystem of F-less than or equal to.