ML modules are great, but I'm not convinced that making them first-class (1ML) will be equally great. ML hits a sweet spot between automation (full type inference) and expressiveness that is only possible because the type language is first-order. This is IMO the point that most extensions on top of Hindley-Milner completely miss.
So, if anything, what I'd like to see is a dependently typed language whose type language is a first-order, computation-free (no non-constructor function application) subset of the value language.
The 1ML papers discuss this, ML implementations in reality are already incomplete with regard to Hindley-Milner, a quote:
"We show how Damas/Milner-style type inference can be integrated into such a language; it is incomplete, but only in ways that are already present in existing ML implementations."
So, if anything, what I'd like to see is a dependently typed language whose type language is a first-order, computation-free (no non-constructor function application) subset of the value language.