> 2) It is not clear whether one can covert a magic instant solver of the halting problem (a "Turing oracle") into a practical solver for the actual outcome of the type inference (since the termination can be of two types: "validated" and "error found").

Actually, this is doable -- one just considers a modified program: which loops, if the original one gave the "error found" answer, or, alternatively, which loops, if the original one gave the "validated" answer, and apply the oracle to those.. Cool!