Inferring (most general, simple) types for lambda terms is a very simple and highly instructive activity. When you try to decipher a lambda term, starting from guessing its type is a very good approach.
The general idea behind type inference is that you start attributing a generic type (a type variable) to any identifier, and then refine this type according to the use you make of the identifier inside the term. This is very easy in the lambda calculus, since an identifier can only be used in two ways: as an argument for a function or as a function.
For instance, in your example, suppose x: α and y: β. But x is applied to y,
hence it must have a functional type, and moreover its input must be compatible with the type of the argument y, hence we refine α to (β -> γ), where γ is the (so fa unknown) result type of the application (x y).
The term (x y) is in turn applied to y. This implies that γ must actually be a functional type too, that is, say, γ = β -> δ.
This essentially concludes the analysis, in this case.
I report below the type of all subterms, for clarity (please, observe that all applications are well typed):
x : β -> β -> γ
y : β
(x y) : β -> γ
((x y) y) : γ
\y.((x y) y) : β -> γ
\x.\y.((x y) y) : (β -> β -> γ) -> β -> γ
Additionally, we conclude g:β -> β -> γ, and h:β.
The whole expression has type γ.
A slightly more interesting example is provided by the term
\y.\x.(y (y x)).
Suppose x: α. Then y must have type α -> β where β is the type of the result (y x). This term is passed again as an input to y, that means that α=β.
So,
\y.\x.(y (y x)) : (α -> α) -> α -> α
In general, in some cases, when you have multiple uses of a same identifier, you will need need to unify their types, inferring the most general instance between them.
The wikipage about the Damas-Milner type inference algorithm is reasonably fine, but in my opinion exceedingly technical for such a simple and intuitive topic.
