Lambda the Ultimate

Suppose a small language with a few primitive types (number, boolean, string) and first-class procedures from and to these types with arbitrary but fixed arity, and the usual syntax (if, let, top-level definitions), but without type declarations. And suppose that the types of all primitive procedures (which are monomorphic) are given, and so is the type of the top-level procedure ("main", a procedure that is not invoked by any procedure, also monomorphic). The language is strict, if it matters.

What I'd like to have is an algorithm that can find the unique monomorphic type of all other procedures in a closed program, or prove that there is none. For example, in main = λ() f0; f = λ(x) gx; g = λ(x) fx, the procedures f and g have no unique monomorphic type, despite being Hindley-Milner typeable. So far I have figured out how to type a fair number of special cases, but I have no clue when to stop looking, or what to do when I run out of heuristics. It's definitely important that procedures can have procedure-valued arguments whose exact types (not merely the fact of being a procedure) must be reconstructed; without those, the problem is easily solved.

Can anyone help?

(Update: Actually, I'm wrong; that example is typeable. As I said, it's procedure-valued arguments that create problems.)