PR Stanley:
f x = x x :: a f x :: b therefore f :: a -> b x = a and x = b therefore a = b therefore f :: a -> a Simple mappings are easy to work out. It's the more detailed stuff I'm not sure about.
You've got the right idea. Type inference involves a process called unification. This is essentially what you are doing when you say "x = a and x = b therefore a = b". (But note that it might be more precise to write x :: a and x :: b therefore a ~ b). Generalising to more complex definitions is just a matter of applying this technique systematically. Just be careful to use a fresh name whenever you introduce a type variable.
f g x y = g x (y x)
On the LHS, f takes 3 parameters, so f :: a -> b -> c -> d, with g :: a, x :: b, y :: c. On the RHS, g takes 2 parameters, the first x :: b, the second y x :: e, and returns the same type as f, so g :: b -> e -> d. Looking at y, it takes one parameter, x :: b, and returns y x :: e, so y :: b -> e. Putting it all together, a ~ (b -> e -> d), c ~ (b -> e), and f :: (b -> e -> d) -> b -> (b -> e) -> d. An automated type checker would need to be more systematic than me, but that should get you started. It gets a little more interesting when you end up with a constraint like this: a Int ~ [b]. In this case, a ~ [] and b ~ Int.