Are the following forms for modular explicit planned to be supported?
val x : ((module A : A)) -> unit
val x' : ((module A : A) as 'a) -> 'a t -> unit
val x'' : (module A : A) t -> A.t -> unit
Right now, it seems that the modules are a sort of special case in the type expression, and don’t follow the normal rules.
A modular explicit is not a general type, it only makes sense as a function parameter so it is forbidden everywhere else. The first two cases should work with regular first-class module types (i.e. (module A) instead of (module A : A)), but the third one cannot work.
During the work on modular explicits, the feature was often called “dependent functions” instead, and if you think about it like that the restriction makes sense. Thinking about module scopes can also help a bit: a dependent parameter binds the corresponding module name in the rest of the type. If you had nested dependent patterns, the scope would be unclear. You could try to lift it to the next enclosing function parameter, but that looks wrong to me (i.e. (module A : A) option -> A.t doesn’t look like a valid type to me: if you pass None to the function, the result cannot be typed.