Title: Typability is Undecidable for F+Eta
Author: J. B. Wells
Date: March 9, 1996
Abstract:
System F is the well-known polymorphically-typed lambda calculus with
universal quantifiers. F+eta is System F extended with the eta rule,
which says that if term M can be given type tau and M eta-reduces to N ,
then N can also be given the type tau. Adding the eta rule to System F is
equivalent to adding the subsumption rule using the subtyping
(containment) relation that Mitchell defined and axiomatized [Mit88]. The
subsumption rule says that if M can be given type tau and tau is a subtype
of type sigma, then M can be given type sigma. Mitchell's subtyping
relation involves no extensions to the syntax of types, i.e., no bounded
polymorphism and no supertype of all types, and is thus unrelated to the
system "F-sub".
Typability for F+eta is the problem of determining for any term M whether
there is any type tau that can be given to it using the type inference
rules of F+eta. Typability has been proven undecidable for System F
[Wel94] (without the eta rule), but the decidability of typability has
been an open problem for F+eta. Mitchell's subtyping relation has
recently been proven undecidable [TU95,Wel95b], implying the
undecidability of "type checking" for F+eta. This paper reduces the
problem of subtyping to the problem of typability for F+eta, thus proving
the undecidability of typability. The proof methods are similar in
outline to those used to prove the undecidability of typability for System
F, but the fine details differ greatly.