Thanks. That's really interesting. I need to read MacQueen's paper. Is this full HKT, in the sense that all constructions wiht HKTs can be encoded in MacQueen's system?

If by "all constructions wiht HKTs", you mean what can be done with HKTs in Haskell, then I'd say yes. It is well-known that ML modules provide a very advanced level of expressiveness, especially since OCaml's introduction of first-class modules. Also, Scala took this idea further and provides principled recursive first-class modules (which Scala calls dependent object types).

The problem is that modules in ML have a verbose syntax and are clunky to use compared to type classes. OCaml's modular implicits aim to make this better (see https://arxiv.org/abs/1512.01895), taking inspiration from Sala's implicits.

I understand that making modules first-class gives them a lot of expressivity. But they are a fairly recent development" at least in OCaml the come much after Haskell. But are modules in MacQueen's sense first-class?