Comment author: @garrigue

While this is a soundness issue, one really has to go through all these steps to trigger it, so it is not that urgent.

Comment author: @lpw25

I think this would be fixed if module type of always returned the strengthened module type. Although it's probably still not great to have modules with ill-formed module types.

Comment author: @lpw25

Just for clarity, the example without functor application or GADTs:

module F(X : sig type t end) = struct
type x = X.t
type y = X.t
type t = E of x
type u = t = E of y
end;;

module M = F(struct type t end);;

module type S = module type of M;;

module rec M1 : S with type x = int and type y = bool = M1;;

let bool_of_int x =
let (E y : M1.u) = (E x : M1.t) in
y;;

bool_of_int 3;;

Comment author: @garrigue

I think this would be fixed if module type of always returned the strengthened module type.

Indeed I expected this comment, which is very true. Unfortunately, as long as we do not drop completely the compatibility mode, the problem will stay around.

Thanks for the example without GADTs. Since we're just relying on the local equality, there is indeed no need for them, meaning that this bug is in OCaml at least since the introduction of module type of (which I think came after module rec, but I may have the order wrong).

This is really the kind of situation where a post-checker, such as Pierrick Couderc's, would come handy.
Not sure how hard it would be to check for well-formedness inside the compiler: equations are used in many places, so this essentially amounts to re-constructing the whole type.

We are not yet sure all instances of this problem are fixed, but the specific example (and @lpw25 's version) are fixed by #8570, commits 4fe08b2 in trunk and 8cb7888 in 4.08.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Since the bug is fixed, let's close this; we can find it again if another problem arises.