Output recursive expressions using Hindley Milner & constraints

Question

I am trying to infer the type of the following expression:

let rec fix f = f (fix f) 

to which type must be assigned (a -> a) -> a

After using the lower level algorithm (described in the generalization of Hindley-Milner type inference algorithms) with the rule added below:

  a1, c1 |-BU e1 : t1 B = fresh var --------------------------------------------------------- a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t 

The following type remains to me: t1 -> t2

and the following restrictions:

 t0 = fix t1 = f t2 = f (fix f) t3 = f t4 = fix f t5 = fix t6 = f t3 = t1 t3 = t4 -> t2 t5 = t0 t5 = t6 -> t4 t6 = t1 

I cannot understand how these restrictions can be solved, so I stay with type (a -> a) -> a . I hope it is obvious to someone that I'm wrong.

full source code here

Answer 1

Shouldn't there be t7 for the first fix f ? They give limitations:

 t7 = t2 t0 = t1 -> t7 

From this you should be able to deduce t4 = t2 , and then t0 = (t2 -> t2) -> t2 .