I asked the relevant people (Leo White, Jacques Garrigue and Frédéric Bour) at ICFP in early September, and I thought that people may be interested in a summary of “where we are right now”. Please remember however that (1) I am not personally working on modular implicits, so I may very well be wrong on various points and (2) Leo, who is working on modular implicits, has provided an explicit non-response indicating in particular that giving detailed explanations on a work-in-progress is taxing. For these reasons, please be considerate in how you respond and whether to ask further questions.
My understanding of the current status is that:
- there is wide consensus that the feature is important and desirable
- there is no consensus, or even clear picture, of whether the type system (module system) changes implied by the feature preserve the desirable properties of the OCaml type system (soundness and principality); Leo says they do, but no one else knows.
The plan for the future is to have (1) a theory of the feature that people agree on and (2) a type-checker that implements this theory. Right now, Leo provided a draft of (1), but it is substantially more powerful/complex than what the OCaml type-checker currently implements. We need to bridge that gap, by making the theory simpler, or the type-checker beefier, probably a bit of both.
One reason why this takes time is that this is very specialized work, with only a handful of people with both (1) the skillset to work on this and (2) time they are willing to volunteer for this. They are effectively working at the time scale of research, which is a long time scale.