[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The work on extensible sum types (e.g. like the polymorphic variants of OCaml) could be interesting for you if you don’t know about it already. A notable work on this is “A polymorphic record calculus and its compilation” by Ohori (TOPLAS 1995), though it doesn’t discuss recursive types. A more recent one is “Extensible programming with first-class cases” by Blume, Acar, and Chae (ICFP 2006).
These works, however, do not have true subtyping but use unification with a notion of kinding for type variables (Ohori) or row variables (Blume et al.).
In our work at ICFP 2016 ("Set-theoretic types for polymorphic variants” by Castagna, Petrucciani, and Nguyen) we have described type inference for a type system with polymorphic variant types, union types, and recursive types, with subtyping based on the “semantic subtyping” approach.
A revised version of that type inference system will be described in Tommaso Petrucciani’s forthcoming PhD thesis (it is currently in the hands of the reviewers, but I can send you a copy via PM if you wish). This is a major revision of our ICFP paper. In particular the proof of completeness there was not correct, and the thesis addresses this issue (by using techniques introduced in Dolan's thesis already cited in previous messages) and provides a more robust solution.
Cheers Beppe
