For the record: I think this is a good question, and I have made sure to relay it to people working on modular explicits in the past (nowadays: @lpw25, @didierremy, @samsa1). After some discussions there is a new consensus that merging modular-explicits and first-class modules is the way to go, as suggested/hinted by @EduardoRFS above.
A function that takes a module as parameter may:
- either be dependent (the name of the module is used in the right-hand-side of the arrow), and it can only be passed arguments that are module paths (“pure module expressions”)
- or be non-dependent, and it can also be passed arguments that are dynamically computed, for example
if ... then (module ...) else (module ...).
If a user does not know/understand the difference between the two, they can just write code using the same user-facing feature, and they will get an error message if they try to use the combination that is invalid (dependent type with dynamic arguments). I think that the resulting system is simpler to use, instead of having to decide a-priori which of two different mechanisms to use.