Typed Lambda Calculus

I want to find the type of the lambda expression \x y -> x y y. I proceed as follows.

1. We go in the reverse order of operations and "unpack" the expression. Assume the whole expression has type A. Then let y have type x1 and \x y -> x y have type B. Then A = B -> x1
2. We already know the type of y, and let \x y -> x be of the type C. Then B = C -> x1.
3. The type of \x y -> x is obviously x1->x2->x1. This is given to us in the previous exercise and makes sense because this expression takes in two arguments and returns the first.

Putting it all together we have that:

A = B -> x1 = C -> x1 -> x1 = (x1 -> x2 -> x1) -> x1 -> x1

The correct answer is somehow:

(x1 -> x1 -> x2) -> x1 -> x2 

What am I doing wrong?

>Solution :

Here I just write stuff’s types under it and go from there:

foo = \x   y ->   x   y    y
foo    x   y =    x   y    y 
       a   b                 :  c
                  a   b    b :  c
                  a   b :  b -> c
                  a : b -> b -> c
foo : a -> b -> c
    ~ (b -> b -> c) -> b -> c