Add a test and fix for issue #13955

[voodoos]

The bug was most certainly introduced in #13308

So far I have not been able to provide a fix that doesn't break other unused warnings.

[Octachron]

I think you can add the new test directly inside the w32.ml file.

[voodoos]

I bisected it to: 14e3ff3

[voodoos]

I added a possible fix in d0d07ba

[Octachron]

It would be closer to the specification that I had in mind to use unknow ~mark:true for the mark_both:true case. Indeed, we are using the Includemod.modtypes function to compare two module types at the source level.
Thus we are rather in the positive case rather than the strictly positive case where we compare the module type of a source level module with a (source-level) module type.

[voodoos]

If I do that I have the following change in the way uids are paired together:

diff

diff --git a/typing/includemod.ml b/typing/includemod.ml
index 7e9da51053..ca4cad1ae3 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -1344,6 +1344,17 @@ let modtypes_with_shape ~shape ~loc env ~mark mty1 mty2 =
   | Ok (cc, shape) -> cc, shape
   | Error reason -> raise (Error (env, Error.(In_Module_type reason)))
 
+let modtypes_constraint ~shape ~loc env ~mark mty1 mty2 =
+  (* modtypes with shape is used when typing module expressions in [Typemod] *)
+  let direction = Directionality.unknown ~mark in
+  match
+    modtypes ~core:core_inclusion ~direction ~loc env Subst.identity
+      mty1 mty2 shape
+  with
+  | Ok (cc, shape) -> cc, shape
+  | Error reason -> raise (Error (env, Error.(In_Module_type reason)))
+
+
 let modtypes_consistency ~loc env mty1 mty2 =
   let direction = Directionality.unknown ~mark:false in
   match
diff --git a/typing/includemod.mli b/typing/includemod.mli
index fbace5a443..1001c2bd53 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -152,6 +152,10 @@ val modtypes_with_shape:
   shape:Shape.t -> loc:Location.t -> Env.t -> mark:bool ->
   module_type -> module_type -> module_coercion * Shape.t
 
+val modtypes_constraint:
+  shape:Shape.t -> loc:Location.t -> Env.t -> mark:bool ->
+  module_type -> module_type -> module_coercion * Shape.t
+
 val strengthened_module_decl:
   loc:Location.t -> aliasable:bool -> Env.t -> mark:bool ->
   module_declaration -> Path.t -> module_declaration -> module_coercion
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 2325673fff..b42de79c7d 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -2194,7 +2194,7 @@ let wrap_constraint_with_shape env mark arg mty
   shape explicit =
   let coercion, shape =
     try
-      Includemod.modtypes_with_shape ~shape ~loc:arg.mod_loc env ~mark
+      Includemod.modtypes_constraint ~shape ~loc:arg.mod_loc env ~mark
         arg.mod_type mty
     with Includemod.Error msg ->
       raise(Error(arg.mod_loc, env, Not_included msg)) in

type t (* 1 *) = int

module type S (* 3 *) = sig
  val y (* 2 *) : t
end

module M (* 5 *) : S = struct
  let y (* 4 *) = 36
end

-Link_intf_impl.4 <- Link_intf_impl.2
+Link_intf_impl.4 <-> Link_intf_impl.2

Isn't that a regression ?

[voodoos]

What should I do about this @Octachron ?

Since it's a regression I expect it should be part of 5.4 and 5.3.1 ?

[Octachron]

Another possible name for not both could be rhs_is_interface, which might be easier to read at call site.

[Octachron]

This bugfix is on my review stack for this afternoon and next week. And yes, since this is a bug fix it should be part of 5.4 .

[Octachron]

Since both users of the function uses mark_both:true, I propose to remove this new argument.
I think we can also improve the name of the function to modtypes_constraint.
We could also add an extended comment, something similar to

(** [modtypes_constraint ~shape ~loc env ~mark exp_modtype constraint_modtype]
    checks that [exp_modtype] is a subtype of [constraint_modtype], and returns
    the module coercion and the shape of the constrained module.

    It also marks as used paired items in positive position in [exp_modtype],
    and also paired items in negative position in [constraint_modtype].

    This marking in negative position allows to raise an [unused item] warning
    whenever an item in a functor parameter in [constraint_modtype] does not
    exist in [exp_modtypes]. This behaviour differs from the one in
    {!check_implementation} and {!compunit} which assumes that is not
    appropriate to raise warning about the interface file while typechecking the
    implementation file.
*) 
val constraint_modtypes:

[Octachron]

Trying to document the reason behind the bug:

In term of usage warnings and in presence of functors, the typechecker make a distinction between checking module inclusion between an implementation and a interface and checking module inclusion between a module expression and a module type in module M = (X : S).

In the first case, we consider that the interface should be fully trusted, thus in

(* a.mli *)
module F(X:sig val x:int) : sig end

(* a.ml *)
module F(X:sig end) = struct end

no warning should be raised about the superfluous val x: int item in the signature of the parameter X in the interface.

Contrarily, when checking a module coercion

module M: sig
  module F(_:sig val x:int) : sig end
end = struct
  module F(_:sig end) = struct end
end

since OCaml 4.07, the typechecker prefers to raise a warning on this superfluous val x:int in the module constraint.

To do so requires to mark as used signature items in the right-hand side of module coercion.
This was the point that I missed in #13308 and which is fixed in this PR.

[Octachron]

I propose to disable warning 60 for this group of module to reduce the noise in the test.

[Octachron]

@voodoos , do you wish to clean up the history or should I merge the PR in its current state?

[voodoos]

@voodoos , do you wish to clean up the history or should I merge the PR in its current state?

Thanks for the review. I squashed some of the commits.