Type constraints and record well-typings
What I thought yesterday ended up being wrong today: Wand's corrigendum was indeed important, and I need to implement another algorithm to type records. In order to find the right algorithm to use for typing my records, today was a reading day.
I studied Rémy's 1989 paper 'Typechecking records and variants in a natural extension of ML' which proposes a solution to Wand's 1987 algorithm's problem. This solution doesn't use normal types but uses 'kinds' instead that add a notion of 'flag' to the standard types which more or less define whether a particular field exists for a particular row. The problem with this solution is that record concatenations are not handled correctly and that it only supports a finite set of labels, known in advance.
I also read Wand's 1991 paper 'Type Inference for Record Concatenation and Multiple Inheritance' which generalises Rémy's algorithm to support concatenation and to solve the label limitation. He uses yet another type representation that adds a notion of constraint, which is a set of equations that a type must solve to be valid.
Finally, I tried pushing further my quest for the ultimate algorithm: after all, if three algorithm have been proposed, there is no reason why there weren't more. However, I didn't really find any algorithm that claimed to be more general than the 1991 Wand algorithm.