A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Question

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?

Answer 1

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.

---

Added 5/9/23:

The example I hint at in the Dowek paper is very simple, so it might be worth outlining it here:

In a calculus with dependent types but no polymorphism (essentially MLTT without inductives or universes), typability of un-annotated terms is somewhat trivial: since the "dependent" part of dependent types can be erased, it suffices to check that the term can be given a simple type!

In contrast, type checking is undecidable, because the dependent types can introduce complex constraints on the inputs of functions.