Writing code again
After more than a week of reading, I have started coding again. I started implementing a type system for a simple lambda calculus with records and variants, that I call SLinks (simple links). The grammar and type inference rules can be found here. All operators on records or variants are applied to only one field at a time, I intend to implement operators on many fields as syntactic sugar. I use a type representation based on Rémy's 1994 paper, but the typing algorithms should be simpler since SLinks does not support free record extension or record concatenation.
I also had news from Limsoon Wong about the typing algorithm he used for Kleisli. He confirms his algorithm doesn't use 'lacks' constraints on fields, or any other fancy typing mechanism (except for the minimalist row variables described in his papers). In order to implement the SLinks syntax (the record extension), the SLinks type system as described above will actually be more complicated than Kleisli's.