I originally opened up an issue on the dotty repo to discuss this, and was asked to move the discussion here. I found this paper on Hacker News today and have read through a few chapters. For me, the lack of full type inference has always been a trade off that I’ve been willing to deal with in order to get the benefits of functional programming with subtype polymorphism. This paper discusses a type system that provides ML style parametric polymorphism, subtype polymorphism, fully decidable type subsumption, and it does it with full type inference.
The author is a member and contributor to the ocaml community and the paper strongly reflects this background but I find a lot of the ideas extremely interesting and would love to see how applicable they are to the DOT calculus and scala in general. In particular I’d love to see how his ideas on biunification fit in with the the DOT calculus, and whether dotty could potentially benefit from these ideas. Also, the paper mentions higher kinder types as future work and was wondering if the ideas used in dotty to build higher minded types on top of DOT could translate over. Feel free to discuss other aspects as they relate to scala as well