We prove that the subtyping problem induced by Mitchell's containment relation (1988) for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption rule.
['Jerzy Tiuryn', 'Pawel Urzyczyn']
The subtyping problem for second-order types is undecidable