From df856b7e559b45a28e93dfbc6f11ac339d49170f Mon Sep 17 00:00:00 2001
From: Chris Casinghino <ccasinghino@janestreet.com>
Date: Fri, 13 Dec 2024 09:23:50 -0500
Subject: [PATCH 1/2] Fix soundness bug in include functor (#3372)

---
 .../include_functor_is_expansive.ml           | 77 +++++++++++++++++++
 typing/typecore.ml                            |  8 +-
 2 files changed, 83 insertions(+), 2 deletions(-)
 create mode 100644 testsuite/tests/typing-modules/include_functor_is_expansive.ml

diff --git a/testsuite/tests/typing-modules/include_functor_is_expansive.ml b/testsuite/tests/typing-modules/include_functor_is_expansive.ml
new file mode 100644
index 00000000000..d45ce9b6d77
--- /dev/null
+++ b/testsuite/tests/typing-modules/include_functor_is_expansive.ml
@@ -0,0 +1,77 @@
+(* TEST
+ flags = "-extension include_functor -w +a";
+ expect;
+*)
+
+(* This is a regression test.  The include functor version of the below program
+   used to typecheck - we check here it gets the same error as the
+   non-include-functor version. *)
+
+module type T = sig
+  type t
+end
+
+module Ref (A : T) : sig
+  val r : A.t option ref
+end = struct
+  let r = ref None
+end;;
+[%%expect{|
+module type T = sig type t end
+module Ref : functor (A : T) -> sig val r : A.t option ref end
+|}]
+
+
+(* Legacy version *)
+let r (type a) =
+  let module R = struct
+    module T = struct
+      type t = a
+    end
+
+    include Ref(T)
+  end
+  in
+  R.r
+;;
+
+let magic (type a b) (a : a) : b =
+  r := Some a;
+  match !r with
+  | Some r -> r
+  | None -> assert false
+;;
+[%%expect{|
+val r : '_a option ref = {contents = None}
+Line 14, characters 12-13:
+14 |   r := Some a;
+                 ^
+Error: This expression has type "a" but an expression was expected of type "'a"
+       The type constructor "a" would escape its scope
+|}]
+
+(* Include functor version *)
+let r (type a) =
+  let module R = struct
+    type t = a
+
+    include functor Ref
+  end
+  in
+  R.r
+;;
+
+let magic (type a b) (a : a) : b =
+  r := Some a;
+  match !r with
+  | Some r -> r
+  | None -> assert false
+;;
+[%%expect{|
+val r : '_a option ref = {contents = None}
+Line 12, characters 12-13:
+12 |   r := Some a;
+                 ^
+Error: This expression has type "a" but an expression was expected of type "'a"
+       The type constructor "a" would escape its scope
+|}]
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 0b4f242fc48..4f4e2bb669e 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -4230,8 +4230,12 @@ and is_nonexpansive_mod mexp =
           | Tstr_value (_, pat_exp_list) ->
               List.for_all (fun vb -> is_nonexpansive vb.vb_expr) pat_exp_list
           | Tstr_module {mb_expr=m;_}
-          | Tstr_open {open_expr=m;_}
-          | Tstr_include {incl_mod=m;_} -> is_nonexpansive_mod m
+          | Tstr_open {open_expr=m;_} -> is_nonexpansive_mod m
+          | Tstr_include {incl_mod=m;incl_kind=k;_} ->
+            begin match k with
+            | Tincl_structure -> is_nonexpansive_mod m
+            | Tincl_functor _ | Tincl_gen_functor _ -> false
+            end
           | Tstr_recmodule id_mod_list ->
               List.for_all (fun {mb_expr=m;_} -> is_nonexpansive_mod m)
                 id_mod_list

From 83b13bed05a05d19144af5867c9736e880d71ab6 Mon Sep 17 00:00:00 2001
From: Zesen Qian <riaqn@users.noreply.github.com>
Date: Fri, 13 Dec 2024 18:20:07 +0000
Subject: [PATCH 2/2] Module inclusion check looks at module mode (#3328)

---
 driver/compile_common.ml                      |   2 +-
 testsuite/tests/typing-modes/md_modalities.ml |   2 +-
 .../tests/typing-modes/val_modalities.ml      | 312 +++++++++++++++++-
 toplevel/byte/topeval.ml                      |   3 +-
 toplevel/native/opttoploop.ml                 |   4 +-
 typing/includecore.ml                         |  38 ++-
 typing/includecore.mli                        |   9 +
 typing/includemod.ml                          |  80 +++--
 typing/includemod.mli                         |   9 +-
 typing/typemod.ml                             |  18 +-
 10 files changed, 418 insertions(+), 59 deletions(-)

diff --git a/driver/compile_common.ml b/driver/compile_common.ml
index 9bd7ef18e88..5aa113d4b32 100644
--- a/driver/compile_common.ml
+++ b/driver/compile_common.ml
@@ -84,7 +84,7 @@ let typecheck_intf info ast =
         Format.(fprintf std_formatter) "%a@."
           (Printtyp.printed_signature (Unit_info.source_file info.target))
           sg);
-  ignore (Includemod.signatures info.env ~mark:Mark_both sg sg);
+  ignore (Includemod.signatures info.env ~mark:Mark_both ~modes:Legacy sg sg);
   Typecore.force_delayed_checks ();
   Builtin_attributes.warn_unused ();
   Warnings.check_fatal ();
diff --git a/testsuite/tests/typing-modes/md_modalities.ml b/testsuite/tests/typing-modes/md_modalities.ml
index e3cd0e71a79..4e64dd01389 100644
--- a/testsuite/tests/typing-modes/md_modalities.ml
+++ b/testsuite/tests/typing-modes/md_modalities.ml
@@ -142,5 +142,5 @@ Error: Signature mismatch:
          val foo : 'a -> 'a
        is not included in
          val foo : 'a -> 'a @@ portable
-       The second is portable and the first is not.
+       The second is portable and the first is nonportable.
 |}]
diff --git a/testsuite/tests/typing-modes/val_modalities.ml b/testsuite/tests/typing-modes/val_modalities.ml
index 22dc31935d9..645f058e348 100644
--- a/testsuite/tests/typing-modes/val_modalities.ml
+++ b/testsuite/tests/typing-modes/val_modalities.ml
@@ -113,7 +113,7 @@ Error: Signature mismatch:
          val x : string @@ global many portable contended
        is not included in
          val x : string
-       The second is empty and the first is contended.
+       The second is uncontended and the first is contended.
 |}]
 
 module Module_type_nested = struct
@@ -160,7 +160,7 @@ Error: Signature mismatch:
          val y : string @@ global many portable contended
        is not included in
          val y : string
-       The second is empty and the first is contended.
+       The second is uncontended and the first is contended.
 |}]
 
 (* When defaulting, prioritize modes in arrow types over modalities. *)
@@ -213,7 +213,7 @@ Error: Signature mismatch:
          val x : string @@ global many portable contended
        is not included in
          val x : string
-       The second is empty and the first is contended.
+       The second is uncontended and the first is contended.
 |}]
 
 module Inclusion_weakens_monadic = struct
@@ -342,7 +342,7 @@ Error: Signature mismatch:
          external length : string -> int = "%string_length"
        is not included in
          external length : string -> int @@ portable = "%string_length"
-       The second is portable and the first is not.
+       The second is portable and the first is nonportable.
 |}]
 
 module M : sig
@@ -461,10 +461,312 @@ Error: Signature mismatch:
          val f : int -> int @@ global many
        is not included in
          val f : int -> int @@ portable
-       The second is portable and the first is not.
+       The second is portable and the first is nonportable.
 |}]
 
 
+(* module inclusion check should look at the modes of the modules, since some
+module type inclusion is only true for certain modes. Currently modules are
+always global many, which allows more module inclusion. *)
+
+(* value description inclusion check look at the modes of the enclosing
+   structure. *)
+module M : sig
+  val foo : 'a -> 'a @@ global many
+end = struct
+  include (struct let foo x = x end : sig val foo : 'a -> 'a end)
+end
+[%%expect{|
+module M : sig val foo : 'a -> 'a @@ global many end
+|}]
+
+(* CR zqian: with non-legacy modules, we will extend the tests to modalities on
+module declarations, instead of relying on modalities on value descriptions to
+tell if the extra modes are considered. *)
+
+(* module declaration inclusion check looks at the mode of the enclosing
+   structure, which in turn affects value description inclusion check. *)
+module M : sig
+  module N : sig val foo : 'a -> 'a @@ global many end
+end = struct
+  module N : sig val foo : 'a -> 'a end = struct let foo x = x end
+end
+[%%expect{|
+module M : sig module N : sig val foo : 'a -> 'a @@ global many end end
+|}]
+
+(* CR zqian: inclusion check should cross modes, if we are comparing modes. *)
+module M : sig
+  module N : sig val foo : int @@ portable end
+end = struct
+  module N = struct let foo @ nonportable = 42 end
+end
+[%%expect{|
+Lines 3-5, characters 6-3:
+3 | ......struct
+4 |   module N = struct let foo @ nonportable = 42 end
+5 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig module N : sig val foo : int @@ global many end end
+       is not included in
+         sig module N : sig val foo : int @@ portable end end
+       In module "N":
+       Modules do not match:
+         sig val foo : int @@ global many end
+       is not included in
+         sig val foo : int @@ portable end
+       In module "N":
+       Values do not match:
+         val foo : int @@ global many
+       is not included in
+         val foo : int @@ portable
+       The second is portable and the first is nonportable.
+|}]
+
+(* module constraint inclusion check looks at the modes of modules *)
+module F (M : sig val foo : 'a -> 'a end) = struct
+  module M' : sig val foo : 'a -> 'a @@ global many end = M
+end
+[%%expect{|
+module F :
+  functor (M : sig val foo : 'a -> 'a end) ->
+    sig module M' : sig val foo : 'a -> 'a @@ global many end end
+|}]
+
+(* Similiar for recursive modules *)
+module rec M : sig
+  module N : sig val foo : 'a -> 'a @@ global many end
+end = struct
+  module N : sig val foo : 'a -> 'a end = struct let foo x = x end
+end
+[%%expect{|
+module rec M : sig module N : sig val foo : 'a -> 'a @@ global many end end
+|}]
+
+
+(* functor application inclusion check looks at the modes of parameter and
+   argument *)
+module F (M : sig val f : 'a -> 'a @@ global many end) = struct
+end
+[%%expect{|
+module F : functor (M : sig val f : 'a -> 'a @@ global many end) -> sig end
+|}]
+
+module G (M : sig val f : 'a -> 'a end) = F(M)
+[%%expect{|
+module G : functor (M : sig val f : 'a -> 'a end) -> sig end
+|}]
+
+(* Similiar for [include_functor] *)
+module G (M : sig val f : 'a -> 'a end) = struct
+  include M
+  include functor F
+end
+[%%expect{|
+module G : functor (M : sig val f : 'a -> 'a end) -> sig val f : 'a -> 'a end
+|}]
+
+(* functor declaration inclusion check  looks at the modes of parameter and
+  return*)
+module F : (sig val foo : 'a -> 'a end) -> (sig val bar : 'a -> 'a @@ global many end) =
+functor (M : sig val foo : 'a -> 'a @@ global many end) -> struct let bar = M.foo end
+[%%expect{|
+module F :
+  sig val foo : 'a -> 'a end -> sig val bar : 'a -> 'a @@ global many end
+|}]
+
+(* CR zqian: package subtyping doesn't look at the package mode for simplicity.
+NB: coercion is the only place of subtype checking packages; all other places
+are equality check. *)
+module type S = sig val foo : 'a -> 'a @@ global many end
+module type S' = sig val foo : 'a -> 'a end
+
+let f (x : (module S)) = (x : (module S) :> (module S'))
+[%%expect{|
+module type S = sig val foo : 'a -> 'a @@ global many end
+module type S' = sig val foo : 'a -> 'a end
+val f : (module S) -> (module S') @@ global many = <fun>
+|}]
+
+let f (x : (module S')) = (x : (module S') :> (module S))
+[%%expect{|
+Line 1, characters 26-57:
+1 | let f (x : (module S')) = (x : (module S') :> (module S))
+                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type "(module S')" is not a subtype of "(module S)"
+|}]
+
+(* module equality/substitution inclusion check looks at modes of modules, even
+   when inside a module type declaration *)
+module type S = sig
+  module M : sig
+    val foo : 'a -> 'a @@ global many
+  end
+end
+
+module type F = functor (M':sig val foo : 'a -> 'a end) -> sig
+  module Subst : sig
+    module type S' = S with module M := M'
+
+    module M'' : sig val foo : 'a -> 'a end
+    module type S'' = S with module M := M''
+  end
+
+  module Eq : sig
+    module type S' = S with module M = M'
+
+    module M'' : sig val foo : 'a -> 'a end
+    module type S'' = S with module M := M''
+  end
+end
+
+[%%expect{|
+module type S = sig module M : sig val foo : 'a -> 'a @@ global many end end
+module type F =
+  functor (M' : sig val foo : 'a -> 'a end) ->
+    sig
+      module Subst :
+        sig
+          module type S' = sig end
+          module M'' : sig val foo : 'a -> 'a end
+          module type S'' = sig end
+        end
+      module Eq :
+        sig
+          module type S' = sig module M : sig val foo : 'a -> 'a end end
+          module M'' : sig val foo : 'a -> 'a end
+          module type S'' = sig end
+        end
+    end
+|}]
+
+(* strenghtening inclusion check looks at module modes, even inside a module
+  type declaration. *)
+module type F = functor (M : sig val foo : 'a -> 'a end) -> sig
+  module type S = sig val foo : 'a -> 'a @@ global many end with M
+end
+[%%expect{|
+module type F =
+  functor (M : sig val foo : 'a -> 'a end) ->
+    sig module type S = sig val foo : 'a -> 'a @@ global many end end
+|}]
+
+
+(* module type declaration inclusion check doesn't look at the enclosing
+   structure's mode, because that mode is irrelevant. *)
+module M : sig
+  module type S = sig val foo : 'a end
+end = struct
+  module type S = sig val foo : 'a @@ global many end
+end
+[%%expect{|
+Lines 3-5, characters 6-3:
+3 | ......struct
+4 |   module type S = sig val foo : 'a @@ global many end
+5 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig module type S = sig val foo : 'a @@ global many end end
+       is not included in
+         sig module type S = sig val foo : 'a end end
+       Module type declarations do not match:
+         module type S = sig val foo : 'a @@ global many end
+       does not match
+         module type S = sig val foo : 'a end
+       The second module type is not included in the first
+       At position "module type S = <here>"
+       Module types do not match:
+         sig val foo : 'a end
+       is not equal to
+         sig val foo : 'a @@ global many end
+       At position "module type S = <here>"
+       Values do not match:
+         val foo : 'a
+       is not included in
+         val foo : 'a @@ global many
+       The second is global_ and the first is not.
+|}]
+
+(* Module declaration inclusion check inside a module type declaration inclusion
+  check. There is no "enclosing module mode" to look at. *)
+module M : sig
+  module type N = sig
+    module M : sig val foo : 'a -> 'a end
+  end
+end = struct
+  module type N = sig
+    module M : sig val foo : 'a -> 'a @@ global many end
+  end
+end
+[%%expect{|
+Lines 5-9, characters 6-3:
+5 | ......struct
+6 |   module type N = sig
+7 |     module M : sig val foo : 'a -> 'a @@ global many end
+8 |   end
+9 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig
+           module type N =
+             sig module M : sig val foo : 'a -> 'a @@ global many end end
+         end
+       is not included in
+         sig
+           module type N = sig module M : sig val foo : 'a -> 'a end end
+         end
+       Module type declarations do not match:
+         module type N =
+           sig module M : sig val foo : 'a -> 'a @@ global many end end
+       does not match
+         module type N = sig module M : sig val foo : 'a -> 'a end end
+       The second module type is not included in the first
+       At position "module type N = <here>"
+       Module types do not match:
+         sig module M : sig val foo : 'a -> 'a end end
+       is not equal to
+         sig module M : sig val foo : 'a -> 'a @@ global many end end
+       At position "module type N = sig module M : <here> end"
+       Modules do not match:
+         sig val foo : 'a -> 'a end
+       is not included in
+         sig val foo : 'a -> 'a @@ global many end
+       At position "module type N = sig module M : <here> end"
+       Values do not match:
+         val foo : 'a -> 'a
+       is not included in
+         val foo : 'a -> 'a @@ global many
+       The second is global_ and the first is not.
+|}]
+
+(* functor type inclusion: the following two functor types are equivalent,
+  because a functor of the first type at any mode, can be zero-runtime casted
+  to the second type at the same mode. Essentially, the parameter and return
+  mode is in the functor type, and doesn't depend on the mode of the functor. *)
+module M : sig
+  module type F = (sig val foo : 'a @@ global many end) ->
+    (sig end)
+end = struct
+  module type F = (sig val foo : 'a end) ->
+    (sig end)
+end
+[%%expect{|
+module M :
+  sig module type F = sig val foo : 'a @@ global many end -> sig end end
+|}]
+
+module M : sig
+  module type F =
+    (sig end) -> (sig val foo : 'a end)
+end = struct
+  module type F =
+    (sig end) -> (sig val foo : 'a @@ global many end)
+end
+[%%expect{|
+module M : sig module type F = sig end -> sig val foo : 'a end end
+|}]
+
 module type T = sig @@ portable
   val foo : 'a -> 'a
   val bar : 'a -> 'a @@ nonportable
diff --git a/toplevel/byte/topeval.ml b/toplevel/byte/topeval.ml
index 03020f0da7a..a4cf53b5851 100644
--- a/toplevel/byte/topeval.ml
+++ b/toplevel/byte/topeval.ml
@@ -125,7 +125,8 @@ let execute_phrase print_outcome ppf phr =
       in
       if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
       let sg' = Typemod.Signature_names.simplify newenv sn sg in
-      ignore (Includemod.signatures ~mark:Mark_positive oldenv sg sg');
+      ignore (Includemod.signatures ~mark:Mark_positive oldenv
+        ~modes:Legacy sg sg');
       Typecore.force_delayed_checks ();
       let shape = Shape_reduce.local_reduce Env.empty shape in
       if !Clflags.dump_shape then Shape.print ppf shape;
diff --git a/toplevel/native/opttoploop.ml b/toplevel/native/opttoploop.ml
index d2557352e12..a586679f584 100644
--- a/toplevel/native/opttoploop.ml
+++ b/toplevel/native/opttoploop.ml
@@ -400,7 +400,9 @@ let execute_phrase print_outcome ppf phr =
       in
       if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
       let sg' = Typemod.Signature_names.simplify newenv names sg in
-      let coercion = Includemod.signatures oldenv ~mark:Mark_positive sg sg' in
+      let coercion =
+        Includemod.signatures oldenv ~mark:Mark_positive ~modes:Legacy sg sg'
+      in
       Typecore.force_delayed_checks ();
       let str, sg', rewritten =
         match str.str_items with
diff --git a/typing/includecore.ml b/typing/includecore.ml
index e2eaca1d547..a4d5cd2bb97 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -43,9 +43,14 @@ type value_mismatch =
   | Type of Errortrace.moregen_error
   | Zero_alloc of Zero_alloc.error
   | Modality of Mode.Modality.Value.error
+  | Mode of Mode.Value.error
 
 exception Dont_match of value_mismatch
 
+type mmodes =
+  | All
+  | Legacy
+
 let native_repr_args nra1 nra2 =
   let rec loop i nra1 nra2 =
     match nra1, nra2 with
@@ -90,6 +95,7 @@ let primitive_descriptions pd1 pd2 =
     native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args
 
 let value_descriptions ~loc env name
+    ~mmodes
     (vd1 : Types.value_description)
     (vd2 : Types.value_description) =
   Builtin_attributes.check_alerts_inclusion
@@ -102,9 +108,26 @@ let value_descriptions ~loc env name
   | Ok () -> ()
   | Error e -> raise (Dont_match (Zero_alloc e))
   end;
-  begin match Mode.Modality.Value.sub vd1.val_modalities vd2.val_modalities with
-  | Ok () -> ()
-  | Error e -> raise (Dont_match (Modality e))
+  begin match mmodes with
+  | All -> begin
+      match Mode.Modality.Value.sub vd1.val_modalities vd2.val_modalities with
+      | Ok () -> ()
+      | Error e -> raise (Dont_match (Modality e))
+      end;
+  | Legacy when (vd1.val_modalities == vd2.val_modalities) ->
+      (* [wrap_constraint_with_shape] invokes inclusion check with identical
+        inferred modalities, which we need to workaround. *)
+      ()
+  | Legacy ->
+      let mmode1, mmode2 = Mode.Value.legacy, Mode.Value.legacy in
+      let mode1 = Mode.Modality.Value.apply vd1.val_modalities mmode1 in
+      let mode2 =
+        Mode.Modality.Value.(Const.apply (to_const_exn vd2.val_modalities) mmode2)
+      in
+      begin match Mode.Value.submode mode1 mode2 with
+      | Ok () -> ()
+      | Error e -> raise (Dont_match (Mode e))
+      end
   end;
   match vd1.val_kind with
   | Val_prim p1 -> begin
@@ -280,6 +303,14 @@ let report_modality_sub_error first second ppf e =
     first
     (print_modality "not") (Atom (ax, left) : Modality.t)
 
+let report_mode_sub_error first second ppf e =
+  let Mode.Value.Error(ax, {left; right}) = e in
+  Format.fprintf ppf "%s is %a and %s is %a."
+    (String.capitalize_ascii second)
+    (Value.Const.print_axis ax) right
+    first
+    (Value.Const.print_axis ax) left
+
 let report_modality_equate_error first second ppf ((equate_step, sub_error) : Modality.Value.equate_error) =
   match equate_step with
   | Left_le_right -> report_modality_sub_error first second ppf sub_error
@@ -330,6 +361,7 @@ let report_value_mismatch first second env ppf err =
         (fun ppf -> Format.fprintf ppf "is not compatible with the type")
   | Zero_alloc e -> Zero_alloc.print_error ppf e
   | Modality e -> report_modality_sub_error first second ppf e
+  | Mode e -> report_mode_sub_error first second ppf e
 
 let report_type_inequality env ppf err =
   Printtyp.report_equality_error ppf Type_scheme env err
diff --git a/typing/includecore.mli b/typing/includecore.mli
index 182ab99741f..dea4a38b4cd 100644
--- a/typing/includecore.mli
+++ b/typing/includecore.mli
@@ -38,6 +38,7 @@ type value_mismatch =
   | Type of Errortrace.moregen_error
   | Zero_alloc of Zero_alloc.error
   | Modality of Mode.Modality.Value.error
+  | Mode of Mode.Value.error
 
 exception Dont_match of value_mismatch
 
@@ -120,8 +121,16 @@ type type_mismatch =
   | Extensible_representation of position
   | Jkind of Jkind.Violation.t
 
+type mmodes =
+  | All
+  (** Check module inclusion [M1 : MT1 @ m1 <= M2 : MT2 @ m2]
+      for all [m1 <= m2]. *)
+  | Legacy
+  (** Check module inclusion [M1 : MT1 @ legacy <= M2 : MT2 @ legacy]. *)
+
 val value_descriptions:
   loc:Location.t -> Env.t -> string ->
+  mmodes:mmodes ->
   value_description -> value_description -> module_coercion
 
 val type_declarations:
diff --git a/typing/includemod.ml b/typing/includemod.ml
index 9f5520dc7a0..37a82bc7915 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -25,6 +25,9 @@ type pos =
   | Arg of functor_parameter
   | Body of functor_parameter
 
+type modes = Includecore.mmodes =
+  | All
+  | Legacy
 
 module Error = struct
 
@@ -139,13 +142,13 @@ let mark_positive = function
 
 (* Inclusion between value descriptions *)
 
-let value_descriptions ~loc env ~mark subst id vd1 vd2 =
+let value_descriptions ~loc env ~mark subst id ~mmodes vd1 vd2 =
   Cmt_format.record_value_dependency vd1 vd2;
   if mark_positive mark then
     Env.mark_value_used vd1.val_uid;
   let vd2 = Subst.value_description subst vd2 in
   try
-    Ok (Includecore.value_descriptions ~loc env (Ident.name id) vd1 vd2)
+    Ok (Includecore.value_descriptions ~loc env (Ident.name id) ~mmodes vd1 vd2)
   with Includecore.Dont_match err ->
     Error Error.(Core (Value_descriptions (diff vd1 vd2 err)))
 
@@ -507,8 +510,8 @@ and shallow_module_paths env subst p1 mty2 p2 =
    described above.
 *)
 
-let rec modtypes ~in_eq ~loc env ~mark subst mty1 mty2 shape =
-  match try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 shape with
+let rec modtypes ~in_eq ~loc env ~mark subst ~modes mty1 mty2 shape =
+  match try_modtypes ~in_eq ~loc env ~mark subst ~modes mty1 mty2 shape with
   | Ok _ as ok -> ok
   | Error reason ->
     let mty1 = Subst.Lazy.force_modtype mty1 in
@@ -517,7 +520,7 @@ let rec modtypes ~in_eq ~loc env ~mark subst mty1 mty2 shape =
     in
     Error Error.(diff mty1 mty2 reason)
 
-and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape =
+and try_modtypes ~in_eq ~loc env ~mark subst ~modes mty1 mty2 orig_shape =
   let open Subst.Lazy in
   (* Do a quick nominal comparison for simple types and if that fails, try to
       unfold one of them. For structured types, do a deep comparison. *)
@@ -539,7 +542,7 @@ and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape =
         begin match Env.find_module_lazy p1 env with
         | md -> begin
             match strengthened_modtypes ~in_eq ~loc ~aliasable:true env ~mark
-                    subst md.md_type p1 mty2 orig_shape
+                    subst ~modes md.md_type p1 mty2 orig_shape
             with
             | Ok _ as x -> x
             | Error reason -> Error (Error.After_alias_expansion reason)
@@ -550,7 +553,7 @@ and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape =
     end
   | (Mty_signature sig1, Mty_signature sig2) ->
       begin match
-        signatures ~in_eq ~loc env ~mark subst sig1 sig2 orig_shape
+        signatures ~in_eq ~loc env ~mark subst ~modes sig1 sig2 orig_shape
       with
       | Ok _ as ok -> ok
       | Error e -> Error (Error.Signature e)
@@ -575,7 +578,9 @@ and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape =
             in
             var, Shape.app orig_shape ~arg:shape_var
       in
-      let cc_res = modtypes ~in_eq ~loc env ~mark subst res1 res2 res_shape in
+      let cc_res =
+        modtypes ~in_eq ~loc env ~mark subst res1 res2 res_shape ~modes:Legacy
+      in
       begin match cc_arg, cc_res with
       | Ok Tcoerce_none, Ok (Tcoerce_none, final_res_shape) ->
           let final_shape =
@@ -631,7 +636,7 @@ and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape =
     in
     match red with
     | Some (mty1,mty2) ->
-        try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 orig_shape
+        try_modtypes ~in_eq ~loc env ~mark subst ~modes mty1 mty2 orig_shape
     | None ->
         (* Report error *)
         match mty1, mty2 with
@@ -672,7 +677,7 @@ and functor_param ~in_eq ~loc env ~mark subst param1 param2 =
       let arg2' = Subst.Lazy.modtype Keep subst arg2 in
       let cc_arg =
         match
-          modtypes ~in_eq ~loc env ~mark Subst.identity arg2' arg1
+          modtypes ~in_eq ~loc env ~mark Subst.identity ~modes:Legacy arg2' arg1
                 Shape.dummy_mod
         with
         | Ok (cc, _) -> Ok cc
@@ -703,20 +708,21 @@ and equate_one_functor_param subst env arg2' name1 name2  =
       env, subst
 
 and strengthened_modtypes ~in_eq ~loc ~aliasable env ~mark
-    subst mty1 path1 mty2 shape =
+    subst ~modes mty1 path1 mty2 shape =
   let mty1 = Mtype.strengthen_lazy ~aliasable mty1 path1 in
-  modtypes ~in_eq ~loc env ~mark subst mty1 mty2 shape
+  modtypes ~in_eq ~loc env ~mark subst ~modes mty1 mty2 shape
 
 and strengthened_module_decl ~loc ~aliasable env ~mark
-    subst md1 path1 md2 shape =
+    subst ~mmodes  md1 path1 md2 shape =
   let md1 = Subst.Lazy.of_module_decl md1 in
   let md1 = Mtype.strengthen_lazy_decl ~aliasable md1 path1 in
   let mty2 = Subst.Lazy.of_modtype md2.md_type in
-  modtypes ~in_eq:false ~loc env ~mark subst md1.md_type mty2 shape
+  let modes = mmodes in
+  modtypes ~in_eq:false ~loc env ~mark subst ~modes md1.md_type mty2 shape
 
 (* Inclusion between signatures *)
 
-and signatures ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
+and signatures ~in_eq ~loc env ~mark subst ~modes sig1 sig2 mod_shape =
   let open Subst.Lazy in
   (* Environment used to check inclusion of components *)
   let sig1 = force_signature_once sig1 in
@@ -745,7 +751,7 @@ and signatures ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
   let paired, unpaired, subst = pair_components subst comps1 sig2 in
   let d =
     signature_components ~in_eq ~loc ~mark new_env subst mod_shape
-      Shape.Map.empty
+      Shape.Map.empty ~mmodes:modes
       (List.rev paired)
   in
   let open Sign_diff in
@@ -769,8 +775,8 @@ and signatures ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
 
 (* Inclusion between signature components *)
 and signature_components :
-  'a. in_eq:_ -> loc:_ -> mark:_ -> _ -> _ -> _ -> _ -> (_ * _ * 'a) list -> 'a Sign_diff.t =
-  fun ~in_eq ~loc ~mark env subst orig_shape shape_map paired ->
+  'a. in_eq:_ -> loc:_ -> mark:_ -> _ -> _ -> _ -> _ -> mmodes:_ -> (_ * _ * 'a) list -> 'a Sign_diff.t =
+  fun ~in_eq ~loc ~mark env subst orig_shape shape_map ~mmodes paired ->
   let open Subst.Lazy in
   match paired with
   | [] -> Sign_diff.{ empty with shape_map }
@@ -780,7 +786,7 @@ and signature_components :
         match sigi1, sigi2 with
         | Sig_value(id1, valdecl1, _) ,Sig_value(_id2, valdecl2, _) ->
             let item =
-              value_descriptions ~loc env ~mark subst id1
+              value_descriptions ~loc env ~mark subst id1 ~mmodes
                 (Subst.Lazy.force_value_description valdecl1)
                 (Subst.Lazy.force_value_description valdecl2)
             in
@@ -816,7 +822,7 @@ and signature_components :
               in
               let item =
                 module_declarations ~in_eq ~loc env ~mark subst id1 mty1 mty2
-                  orig_shape
+                  ~mmodes orig_shape
               in
               let item, shape_map =
                 match item with
@@ -890,7 +896,7 @@ and signature_components :
       let rest =
         if continue then
           signature_components ~in_eq ~loc ~mark env subst
-            orig_shape shape_map rem
+            orig_shape shape_map ~mmodes rem
         else
           let rem = List.map
             (fun (x,y,z) ->
@@ -903,7 +909,7 @@ and signature_components :
        in
        Sign_diff.merge first rest
 
-and module_declarations  ~in_eq ~loc env ~mark  subst id1 md1 md2 orig_shape =
+and module_declarations  ~in_eq ~loc env ~mark  subst id1 ~mmodes md1 md2 orig_shape =
   let open Subst.Lazy in
   Builtin_attributes.check_alerts_inclusion
     ~def:md1.md_loc
@@ -914,7 +920,8 @@ and module_declarations  ~in_eq ~loc env ~mark  subst id1 md1 md2 orig_shape =
   let p1 = Path.Pident id1 in
   if mark_positive mark then
     Env.mark_module_used md1.md_uid;
-  strengthened_modtypes  ~in_eq ~loc ~aliasable:true env ~mark subst
+  let modes = mmodes in
+  strengthened_modtypes  ~in_eq ~loc ~aliasable:true env ~mark subst ~modes
     md1.md_type p1 md2.md_type orig_shape
 
 (* Inclusion between module type specifications *)
@@ -947,6 +954,7 @@ and modtype_infos ~in_eq ~loc env ~mark subst id info1 info2 =
 and check_modtype_equiv ~in_eq ~loc env ~mark mty1 mty2 =
   let c1 =
     modtypes ~in_eq:true ~loc env ~mark Subst.identity mty1 mty2 Shape.dummy_mod
+      ~modes:All
   in
   let c2 =
     (* For nested module type paths, we check only one side of the equivalence:
@@ -957,7 +965,7 @@ and check_modtype_equiv ~in_eq ~loc env ~mark mty1 mty2 =
     else
       let mark = negate_mark mark in
       Some (
-        modtypes ~in_eq:true ~loc env ~mark Subst.identity
+        modtypes ~in_eq:true ~loc env ~mark Subst.identity ~modes:All
           mty2 mty1 Shape.dummy_mod
       )
   in
@@ -976,7 +984,7 @@ let include_functor_signatures ~loc env ~mark subst sig1 sig2 mod_shape =
   let _, _, comps1 = build_component_table (fun _pos name -> name) sig1 in
   let paired, unpaired, subst = pair_components subst comps1 sig2 in
   let d = signature_components ~in_eq:false ~loc ~mark env subst mod_shape
-            Shape.Map.empty
+            Shape.Map.empty ~mmodes:Legacy
             (List.rev paired)
   in
   let open Sign_diff in
@@ -1031,7 +1039,7 @@ exception Apply_error of {
 let check_modtype_inclusion_raw ~loc env mty1 path1 mty2 =
   let aliasable = can_alias env path1 in
   strengthened_modtypes ~in_eq:false ~loc ~aliasable env ~mark:Mark_both
-    Subst.identity mty1 path1 mty2 Shape.dummy_mod
+    Subst.identity ~modes:Legacy mty1 path1 mty2 Shape.dummy_mod
   |> Result.map fst
 
 let check_modtype_inclusion ~loc env mty1 path1 mty2 =
@@ -1070,7 +1078,7 @@ let compunit0
     ~comparison env ~mark impl_name impl_sig intf_name intf_sig unit_shape =
   match
     signatures ~in_eq:false ~loc:(Location.in_file impl_name) env ~mark
-      Subst.identity impl_sig intf_sig unit_shape
+      Subst.identity ~modes:Legacy impl_sig intf_sig unit_shape
   with Result.Error reasons ->
     let diff = Error.diff impl_name intf_name reasons in
     let cdiff =
@@ -1286,7 +1294,7 @@ module Functor_app_diff = struct
             | ( Anonymous | Named _ | Empty_struct ), Named (_, param) ->
                 match
                   modtypes ~in_eq:false ~loc state.env ~mark:Mark_neither
-                    state.subst arg_mty param Shape.dummy_mod
+                    state.subst ~modes:Legacy arg_mty param Shape.dummy_mod
                 with
                 | Error mty -> Result.Error (Error.Mismatch mty)
                 | Ok (cc, _) -> Ok cc
@@ -1306,23 +1314,23 @@ end
 
 (* Hide the context and substitution parameters to the outside world *)
 
-let modtypes_with_shape ~shape ~loc env ~mark mty1 mty2 =
+let modtypes_with_shape ~shape ~loc env ~mark ~modes mty1 mty2 =
   match modtypes ~in_eq:false ~loc env ~mark
-          Subst.identity mty1 mty2 shape
+          Subst.identity ~modes mty1 mty2 shape
   with
   | Ok (cc, shape) -> cc, shape
   | Error reason -> raise (Error (env, Error.(In_Module_type reason)))
 
-let modtypes ~loc env ~mark mty1 mty2 =
+let modtypes ~loc env ~mark ~modes mty1 mty2 =
   match modtypes ~in_eq:false ~loc env ~mark
-          Subst.identity mty1 mty2 Shape.dummy_mod
+          Subst.identity ~modes mty1 mty2 Shape.dummy_mod
   with
   | Ok (cc, _) -> cc
   | Error reason -> raise (Error (env, Error.(In_Module_type reason)))
 
-let signatures env ~mark sig1 sig2 =
+let signatures env ~mark ~modes  sig1 sig2 =
   match signatures ~in_eq:false ~loc:Location.none env ~mark
-          Subst.identity sig1 sig2 Shape.dummy_mod
+          Subst.identity ~modes sig1 sig2 Shape.dummy_mod
   with
   | Ok (cc, _) -> cc
   | Error reason -> raise (Error(env,Error.(In_Signature reason)))
@@ -1343,9 +1351,9 @@ let type_declarations ~loc env ~mark id decl1 decl2 =
       raise (Error(env,Error.(In_Type_declaration(id,reason))))
   | Error _ -> assert false
 
-let strengthened_module_decl ~loc ~aliasable env ~mark md1 path1 md2 =
+let strengthened_module_decl ~loc ~aliasable env ~mark ~mmodes md1 path1 md2 =
   match strengthened_module_decl ~loc ~aliasable env ~mark Subst.identity
-    md1 path1 md2 Shape.dummy_mod with
+    ~mmodes md1 path1 md2 Shape.dummy_mod with
   | Ok (x, _shape) -> x
   | Error mdiff ->
       raise (Error(env,Error.(In_Module_type mdiff)))
diff --git a/typing/includemod.mli b/typing/includemod.mli
index 14ef98e36db..4100f806d98 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -150,19 +150,20 @@ module FieldMap: Map.S with type key = field_desc
 val item_ident_name: Types.signature_item -> Ident.t * Location.t * field_desc
 val is_runtime_component: Types.signature_item -> bool
 
+type modes = Includecore.mmodes
 
 (* Typechecking *)
 
 val modtypes:
-  loc:Location.t -> Env.t -> mark:mark ->
+  loc:Location.t -> Env.t -> mark:mark -> modes:modes ->
   module_type -> module_type -> module_coercion
 
 val modtypes_with_shape:
-  shape:Shape.t -> loc:Location.t -> Env.t -> mark:mark ->
+  shape:Shape.t -> loc:Location.t -> Env.t -> mark:mark -> modes:modes ->
   module_type -> module_type -> module_coercion * Shape.t
 
 val strengthened_module_decl:
-  loc:Location.t -> aliasable:bool -> Env.t -> mark:mark ->
+  loc:Location.t -> aliasable:bool -> Env.t -> mark:mark -> mmodes:modes ->
   module_declaration -> Path.t -> module_declaration -> module_coercion
 
 val check_modtype_inclusion :
@@ -175,7 +176,7 @@ val check_modtype_inclusion :
 val check_modtype_equiv:
   loc:Location.t -> Env.t -> Ident.t -> module_type -> module_type -> unit
 
-val signatures: Env.t -> mark:mark ->
+val signatures: Env.t -> mark:mark -> modes:modes ->
   signature -> signature -> module_coercion
 
 val include_functor_signatures : Env.t -> mark:mark ->
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 1d1eeb2bf4c..0674677a654 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -815,7 +815,7 @@ let merge_constraint initial_env loc sg lid constr =
         in
         let md'' = { md' with md_type = mty } in
         let newmd = Mtype.strengthen_decl ~aliasable:false md'' path in
-        ignore(Includemod.modtypes  ~mark:Mark_both ~loc sig_env
+        ignore(Includemod.modtypes  ~mark:Mark_both ~loc sig_env ~modes:Legacy
                  newmd.md_type md.md_type);
         return
           ~replace_by:(Some(Sig_module(id, pres, newmd, rs, priv)))
@@ -826,7 +826,7 @@ let merge_constraint initial_env loc sg lid constr =
         let aliasable = not (Env.is_functor_arg path sig_env) in
         ignore
           (Includemod.strengthened_module_decl ~loc ~mark:Mark_both
-             ~aliasable sig_env md' path md);
+             ~aliasable sig_env ~mmodes:Legacy md' path md);
         real_ids := [Pident id];
         return ~replace_by:None
           (Pident id, lid, Some (Twith_modsubst (path, lid')))
@@ -1711,7 +1711,7 @@ and transl_modtype_aux env smty =
       let aliasable = not (Env.is_functor_arg path env) in
       try
         ignore
-          (Includemod.modtypes ~loc env
+          (Includemod.modtypes ~loc env ~modes:Legacy
             ~mark:Includemod.Mark_both md.md_type tmty.mty_type);
         mkmty
           (Tmty_strengthen (tmty, path, mod_id))
@@ -2408,7 +2408,7 @@ let check_recmodule_inclusion env bindings =
           try
             Includemod.modtypes_with_shape ~shape
               ~loc:modl.mod_loc ~mark:Mark_both
-              env mty_actual' mty_decl'
+              env ~modes:Legacy mty_actual' mty_decl'
           with Includemod.Error msg ->
             raise(Error(modl.mod_loc, env, Not_included msg)) in
         let modl' =
@@ -2486,6 +2486,8 @@ let modtype_of_package env loc p fl =
   in
   Subst.modtype Keep Subst.identity mty
 
+(* CR zqian: [package_subtype] should take [modes], but piping this through
+  [ctype] is too much. Instead, we take the conservative approach. *)
 let package_subtype env p1 fl1 p2 fl2 =
   let mkmty p fl =
     let fl =
@@ -2496,7 +2498,7 @@ let package_subtype env p1 fl1 p2 fl2 =
   | exception Error(_, _, Cannot_scrape_package_type _) -> false
   | mty1, mty2 ->
     let loc = Location.none in
-    match Includemod.modtypes ~loc ~mark:Mark_both env mty1 mty2 with
+    match Includemod.modtypes ~loc ~mark:Mark_both env ~modes:All mty1 mty2 with
     | Tcoerce_none -> true
     | _ | exception Includemod.Error _ -> false
 
@@ -2508,7 +2510,7 @@ let wrap_constraint_package env mark arg mty explicit =
   let mty2 = Subst.modtype Keep Subst.identity mty in
   let coercion =
     try
-      Includemod.modtypes ~loc:arg.mod_loc env ~mark mty1 mty2
+      Includemod.modtypes ~loc:arg.mod_loc env ~mark ~modes:Legacy mty1 mty2
     with Includemod.Error msg ->
       raise(Error(arg.mod_loc, env, Not_included msg)) in
   { mod_desc = Tmod_constraint(arg, mty, explicit, coercion);
@@ -2523,7 +2525,7 @@ let wrap_constraint_with_shape env mark arg mty
   let coercion, shape =
     try
       Includemod.modtypes_with_shape ~shape ~loc:arg.mod_loc env ~mark
-        arg.mod_type mty
+        ~modes:Legacy arg.mod_type mty
     with Includemod.Error msg ->
       raise(Error(arg.mod_loc, env, Not_included msg)) in
   { mod_desc = Tmod_constraint(arg, mty, explicit, coercion);
@@ -2836,6 +2838,7 @@ and type_one_application ~ctx:(apply_loc,sfunct,md_f,args)
       let coercion =
         try Includemod.modtypes
               ~loc:arg.mod_loc ~mark:Mark_both env arg.mod_type mty_param
+              ~modes:Legacy
         with Includemod.Error _ -> apply_error ()
       in
       let mty_appl =
@@ -2867,6 +2870,7 @@ and type_one_application ~ctx:(apply_loc,sfunct,md_f,args)
             begin match
               Includemod.modtypes
                 ~loc:app_loc ~mark:Mark_neither env mty_res nondep_mty
+                ~modes:Legacy
             with
             | Tcoerce_none -> ()
             | _ ->