How should I type this lambda expression?

Question

Let $M = \lambda xy.xyy$.

How can I type the $\lambda$-term $M$ in simple type theory?

I couldn't find the typing definition cases anywhere, so I don't know where to begin...

Answer 1

The head variable $x$ is applied twice to the same argument $y$, hence the most general type of $x$ has the form $A \to (A \to B)$, for any types $A$ and $B$ such that $A$ is the type of $y$. This entails that the most general type of $xyy$ is $B$. Therefore, the most general type of $\lambda x y. x yy$ is $(A \to (A \to B)) \to (A \to B)$.