Occurs check needed

[yallop]

Expressions with (what would be) recursive types cause the type checker to loop, e.g.

#type let rec f x = f in f;;

[andrejbauer]

Which version is this?

[yallop]

This is with the master HEAD (8eaf328)

[matijapretnar]

I did not get around to implementing it yet because occurs check is a bit more complicated in the presence of subtyping.

Inference is done by building a constraint graph between type parameter. Say that you already have α ≤ β in your constraint graph and you try to add β → γ ≤ α. You need to replace α with some fresh α1 → α2 and add β ≤ α1 and γ ≤ α2 to the graph. But now you need to re-add α ≤ β, which is now α1 → α2 ≤ β and the whole thing repeats.

So you do not only have to check if a variable α occurs in the body on the other side of ≤, but also if any variable in relation with α occurs there. This is probably enough, but I did not think it out fully yet. For an alternative approach, you can take a look at Simonet's paper: "Type inference with structural subtyping: A faithful formalization of an efficient constraint solver"