It's starting to look pretty
If one doesn't use variants (why would anyone do that?), the typing-algorithm works beautifully now. It is able to calculate lovely types like (#tata:pre['23], '22) -> ('22) (the function from a record with field '#tata' and possibly more to a record with the same possibly more). Unfortunately, the expression fun v . case v of <#tata = x>.x | y.y;, which should receive type <#tata:pre[<'1>], '1> -> <'1> doesn't. But I am pretty sure there is just a unification or substitution missing in the variant selection part of algorithm W. Too late to find it tonight though, but I hope to have the whole thing working early tomorrow.