TIL why languages with module systems like OCaml & SML can't have higher-kinded type polymorphism: it makes type unification ~impossible.
Of course, you can use modules & functors, but there's another solution: type-level defunctionalization!
ocamllabs.io/higher/lightwe
Conversation
Replying to
By “why languages with module systems like OCaml & SML” do you also include the constraint that they require full program type inference? I was under the impression that if you gave into dome type annotations, bidirectional inference could help here - could be mistaken though.

