I don't remember enough of the proof for system F to say whether halting problem reduces to it, although usually the proofs are made in such a fashion that it would, and then, in the third sense, we would have an equivalence..

BTW, if we know that type inference for a program in system F nonterminates, does this tell us anything about the program?