Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a proof due to Malecki 1989 that type checking implies typability. This is because exists $\sigma$ such that $M:\sigma$is equivalent to$(\lambda xy.y)M : (\alpha\rightarrow\alpha)$(This is because if a term is typable in System F then all its subterms are.)Is there a simple proof the other way around? That is, a proof that typability implies type checking in System F?
A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?
lo.logic;computability;type theory;lambda calculus;type inference
As far as I know, showing that this direction is the hard part of Wells proof! At least this is what Pawel (Urzyczyn) explained to me a few years back.Apparently it is not too hard to show that type checking is undecidable; the hard part is showing that this implies undecidability of type reconstruction! Indeed there are some cases in which the first is undecidable and the second decidable: see e.g. Dowek 1993.