F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexities they bring.