Type-level module alias for functor parameter accepted

[goldfirere]

The following module is accepted:

module type S1 = sig end

module type S2 = functor (X : S1) -> sig module M = X end

This contradicts https://v2.ocaml.org/manual/modulealias.html, which says that the right-hand side of a module M = M0 in a signature cannot be a functor parameter.

I tried weakly to get this to actually misbehave (accept a program that's clearly not type safe) but was unable to do so. But I think my S2 is uninhabited: I was unable to find a module expression with type S2.

[garrigue]

Indeed, there is no check in transl_modtype_aux that aliases are not functor parameters.
Since this is checked for concrete functor, there should be no soundness, but it would be probably nicer to have an error here, rather than silently accepting an impossible type.

[clementblaudeau]

This issue, which is closely linked to #11441 and #11442, is not completely fixed by #13192 unfortunately. Indeed, aliases to functor parameters can still be obtained indirectly:

module type T = sig module X : sig end module type Alias = sig module X' = X end end;;
module F (Y : T)(Y':Y.Alias) = Y'

returns :

module type T = sig module X : sig end module type Alias = sig module X' = X end end
module F : (Y : T) (Y' : Y.Alias) -> sig module X' = Y.X end

It works because when the alias module X' = X is defined, X is not (yet) a functor parameter. Therefore, no error is thrown and an alias to (a submodule of) a functor parameter is returned. Trying to call F results in typechecker crash, probably linked to avoidance. It's unclear if it can be used to get unsoundness.

[clementblaudeau]

Another way to get an alias to a functor parameter is to use first class modules :

module F
    (Y:sig
       module X : sig end
       module type S = sig module Z = X end
       val x : (module S)
     end) =
struct
  include (val Y.x)
end

returns

module F :
  (Y : sig
         module X : sig end
         module type S = sig module Z = X end
         val x : (module S)
       end)
    -> sig module Z = Y.X end

[clementblaudeau]

Overall, I would suggest merging this issue with #11441 and #11442, and having the resulting issue left open. There are still ways to obtain module aliases to functor parameters.

[garrigue]

I can see various ways to fix this, however aren't transparent ascriptions going to allow the aliasing of functor arguments?
In that case, it may not be worth fixing something that is going to become correct anyway.