Typed Lambda Calculus

Question

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?

Answer 1

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

And another one:

bar = \x    y -> x (y   x)
bar    x    y =  x (y   x)
       a    b                        :  c
                 a (b   a)           :  c
                  ---------
                    b   a :  d
                    b : a -> d
                 a :         d       -> c

bar :  a -> b -> c
    ~ (d -> c) -> ( a       -> d) -> c
    ~ (d -> c) -> ((d -> c) -> d) -> c

But,

baz   x = x   x
      a   a   a :  b
          a : a -> b

baz : a -> b
    ~ (a -> b) -> b
    ~ ((a -> b) -> b) -> b
    ~ (((a -> b) -> b) -> b) -> b
    ........

is an "infinite" type, i.e. the process of type derivation never stops.