Post #2191763

This proof is especially tricky because it needs a lot of inversion on typing derivations, and inversions generally don't work. It's nontrivial even to show if λx.t has a function type, then t has the codomain type assuming x has the domain type! In fact, the proof in the paper I referenced happens to contain a bug. There is a lemma without proof, and the paper it cited has a corrected version where the lemma got replaced. I'm not sure if a complete correct proof has been written down anywhere (though I'm sure experts know the proof), since for example the even the corrected version claim that if a function applied to N arguments have a type, then the function itself has a N-fold curried function type. This is false without subtyping rules.