Title: The Undecidability of Mitchell's Subtyping Relationship
Author: J. B. Wells
Date: December 10, 1995

Abstract:
Mitchell defined and axiomatized a subtyping relationship (also known as
containment , coercibility , or subsumption over the types of System F
(with "arrow" and "forall").  This subtyping relationship is quite simple
and does not involve bounded quantification. Tiuryn and Urzyczyn quite
recently proved this subtyping relationship to be undecidable.  This paper
supplies a new undecidability proof for this subtyping relationship.
First, a new syntax-directed axiomatization of the subtyping relationship
is defined.  Then, this axiomatization is used to prove a reduction from
the undecidable problem of semi-unification to subtyping.  The
undecidability of subtyping implies the undecidability of type checking
for System F extended with Mitchell's subtyping, also known as F plus eta.