Lambda the Ultimate

I was putting together a small typechecker with a friend, who argued that the most straightforward way to determine the types of members of a set of mutually recursive functions would be to initially set the types of all to _|_, then up to a fixed point update the var/type environment with what's known about the return type of each function. After that process, if any type association contains _|_ then the type check should fail.

That definition would have rejected something like let rec f x = f x, which in O'Caml has type forall A . forall B . A -> B.

So my question is, are there important functions that my friend's definition leaves out? I know that "Types and Programming Languages" would have us apply fix at the term level, but where can we go with this approach?