Higher-kinded types aren't an absolute necessity, and, in fact, they force you to pick between modularity (abstract types) and type inference: https://news.ycombinator.com/item?id=12331926 . Not a very pleasant choice, a programmer normally wants both.
Yes, I already said they aren't a necessity, though many people like having higher-kinded types. But then ML/Ocaml folks seem to be doing fine without. I personally prefer having HKT because you can then neatly express well known type-classes for implementing functors, applicatives, monads and many others.
You can recover the power of higher-kinded types with higher-order functors (in the ML sense), without sacrificing the compatibility of abstract types and type inference in the core language.
On the other hand, Haskell's type inference algorithm is simply incompatible with abstract types.
I didn't fully understand your explanation last time. Can you give an example of the conflict between modularity and type inference with HKTs in Haskell?
