Sub-module identities inside an applicative functor are actually generative, leading to invalid signatures

[clementblaudeau]

This issue is in two parts, and was discovered by investigating this bug with recursive modules

Loss of applicativity with submodules

First, the applicativity of functors can be broken by using submodules : two applications of the same (applicative) functor to the same argument produce incompatible (yet concrete) types. This comes from the fact that the submodules inside a functor are actually "generative", every application create a new submodule not equal to the others.
A minimal example would be the following :

module F (_: sig end) = struct type t end 

module G (_: sig end) = struct
  module Y = struct end (* identity of Y is generative *)
  type u = F(Y).t (* actually generative *)
end

module X0 = struct end
module X1 = G(X0) 
module X2 = G(X0) 

let f (x:X1.u) = (x:X2.u) (* fails ! *)

It is caused by the lack of a mechanism to track arbitrary aliases between modules (i.e. general transparent ascription), and might be impossible to fix without (?)

Incorrect strengthening

Strengthening is used to rewrite type equality in a signature resulting from a functor application. However, it does so assuming that abstract types are always applicative, i.e. that adding type equalities/manifests is always correct. When using datatypes, this can lead to a situation where two different type definitions being are considered equal while having different constructors, which is is invalid. The signature returned by the typechecker is not wellformed. This can be seen by slightly adapting the previous example :

module F (_: sig end) = struct type t end

module G (_: sig end) = struct
  module Y = struct end (* identity of Y is generative *)
  type u = F(Y).t  (* actually generative *)
  type v = Entry of u (* also generative, but will be strengthened ! (making it applicative) *)
end

module X0 = struct end
module X1 = B(X0)
module X2 = B(X0)

This gives :

module X1 :
  sig module Y : sig end type u = F(Y).t type v = B(X0).v = A of u end
module X2 :
  sig module Y : sig end type u = F(Y).t type v = X1.v = A of u end

which is incorrect as X1.v and X2.v are equal but with different constructors (as X1.u and X2.u are not equal)
This could be fixed by re-checking the signature after strengthening, but that seems overkill (and costly). An other option would be to try to identify which types inside an applicative functor are actually generative, and prevent strengthening when they appear in the constructors of a datatype. It seems hard and fragile.