"module type of" zap modalities to floor (ocaml-flambda#3922)

Author: riaqn

testsuite/tests/typing-modes/val_modalities.ml

@@ -73,18 +73,48 @@ module Module_type_of_comonadic = struct
     module M = struct
         let x @ portable = fun x -> x
     end
-    (* for comonadic axes, we default to id = meet_with_max, which is the
-    weakest. *)
+    (* for comonadic axes, we default to meet_with_min, which is the strongest.
+    *)
     module M' : module type of M = struct
         let x @ portable = fun x -> x
     end
     let _ = portable_use M.x (* The original inferred modality is zapped *)
 end
 [%%expect{|
-Line 10, characters 25-28:
-10 |     let _ = portable_use M.x (* The original inferred modality is zapped *)
-                              ^^^
-Error: This value is "nonportable" but expected to be "portable".
+module Module_type_of_comonadic :
+  sig
+    module M : sig val x : 'a -> 'a @@ stateless end
+    module M' : sig val x : 'a -> 'a @@ stateless end
+  end
+|}]
+
+(* zapping behavior can cause type error that shouldn't happen in upstream ocaml *)
+module Module_type_of_error = struct
+  module M = struct
+    let x = fun x -> x
+  end
+
+  module M' : module type of M = struct
+    let y = ref 42
+    let x = fun x -> ignore !y; x
+  end
+end
+[%%expect{|
+Lines 6-9, characters 33-5:
+6 | .................................struct
+7 |     let y = ref 42
+8 |     let x = fun x -> ignore !y; x
+9 |   end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val y : int ref val x : 'a -> 'a end
+       is not included in
+         sig val x : 'a -> 'a @@ stateless end
+       Values do not match:
+         val x : 'a -> 'a
+       is not included in
+         val x : 'a -> 'a @@ stateless
+       The second is portable and the first is nonportable.
 |}]
 
 module Module_type_of_monadic = struct
@@ -95,13 +125,28 @@ module Module_type_of_monadic = struct
     (* for monadic axes, we try to push to the id = join_with_min. The original
     modality is pushed to floor. *)
     module M' : module type of M = struct
-        let x @ contended = ref "hello"
+        let x  @ contended = ref "hello"
     end
 end
 [%%expect{|
 Lines 8-10, characters 35-7:
  8 | ...................................struct
- 9 |         let x @ contended = ref "hello"
+ 9 |         let x  @ contended = ref "hello"
+10 |     end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val x : string ref @@ contended end
+       is not included in
+         sig val x : string ref @@ stateless end
+       Values do not match:
+         val x : string ref @@ contended
+       is not included in
+         val x : string ref @@ stateless
+       The second is uncontended and the first is contended.
+|}, Principal{|
+Lines 8-10, characters 35-7:
+ 8 | ...................................struct
+ 9 |         let x  @ contended = ref "hello"
 10 |     end
 Error: Signature mismatch:
        Modules do not match:
@@ -123,28 +168,65 @@ module Module_type_nested = struct
         end
     end
     module M' : module type of M = struct
-        let x @ nonportable = fun t -> t
+        let x @ portable = fun t -> t
         module N = struct
             let y @ contended = ref "hello"
         end
     end
 end
+(* CR zqian: Need to add mode crossing at binding to remove the principality
+issue. See
+https://github.com/ocaml-flambda/flambda-backend/pull/3922#discussion_r2059000469
+*)
 [%%expect{|
 Lines 8-13, characters 35-7:
  8 | ...................................struct
- 9 |         let x @ nonportable = fun t -> t
+ 9 |         let x @ portable = fun t -> t
+10 |         module N = struct
+11 |             let y @ contended = ref "hello"
+12 |         end
+13 |     end
+Error: Signature mismatch:
+       Modules do not match:
+         sig
+           val x : 'a -> 'a @@ stateless
+           module N : sig val y : string ref @@ contended end
+         end
+       is not included in
+         sig
+           val x : 'a -> 'a @@ stateless
+           module N : sig val y : string ref @@ stateless end
+         end
+       In module "N":
+       Modules do not match:
+         sig val y : string ref @@ contended end
+       is not included in
+         sig val y : string ref @@ stateless end
+       In module "N":
+       Values do not match:
+         val y : string ref @@ contended
+       is not included in
+         val y : string ref @@ stateless
+       The second is uncontended and the first is contended.
+|}, Principal{|
+Lines 8-13, characters 35-7:
+ 8 | ...................................struct
+ 9 |         let x @ portable = fun t -> t
 10 |         module N = struct
 11 |             let y @ contended = ref "hello"
 12 |         end
 13 |     end
 Error: Signature mismatch:
        Modules do not match:
          sig
-           val x : 'a -> 'a
+           val x : 'a -> 'a @@ stateless
            module N : sig val y : string ref @@ contended end
          end
        is not included in
-         sig val x : 'a -> 'a module N : sig val y : string ref end end
+         sig
+           val x : 'a -> 'a @@ stateless
+           module N : sig val y : string ref end
+         end
        In module "N":
        Modules do not match:
          sig val y : string ref @@ contended end

testsuite/tests/typing-modules/aliases.ml

@@ -663,7 +663,10 @@ module type S =
   sig
     module N : sig module I = Int end
     module P :
-      sig module I : sig type t = int val compare : 'a -> 'a -> int end end
+      sig
+        module I :
+          sig type t = int val compare : 'a -> 'a -> int @@ portable end
+      end
     module Q :
       sig type wrap' = wrap = W of (Set.Make(Int).t, Set.Make(N.I).t) eq end
   end

testsuite/tests/typing-zero-alloc/signatures.ml

@@ -865,7 +865,8 @@ end
 
 [%%expect{|
 module M_base_for_mto : sig val f : int -> int [@@zero_alloc] end
-module type S_base_mto = sig val f : int -> int [@@zero_alloc] end
+module type S_base_mto =
+  sig val f : int -> int @@ portable [@@zero_alloc] end
 module M_mto_base_good : S_base_mto
 Lines 11-13, characters 37-3:
 11 | .....................................struct
@@ -879,7 +880,7 @@ Error: Signature mismatch:
        Values do not match:
          val f : int -> int [@@zero_alloc opt]
        is not included in
-         val f : int -> int [@@zero_alloc]
+         val f : int -> int @@ portable [@@zero_alloc]
        The former provides a weaker "zero_alloc" guarantee than the latter.
 |}]
 
@@ -899,7 +900,8 @@ end
 
 [%%expect{|
 module M_strict_for_mto : sig val f : int -> int [@@zero_alloc strict] end
-module type S_strict_mto = sig val f : int -> int [@@zero_alloc strict] end
+module type S_strict_mto =
+  sig val f : int -> int @@ portable [@@zero_alloc strict] end
 module M_mto_strict_good : S_strict_mto
 Lines 11-13, characters 41-3:
 11 | .........................................struct
@@ -913,7 +915,7 @@ Error: Signature mismatch:
        Values do not match:
          val f : int -> int [@@zero_alloc]
        is not included in
-         val f : int -> int [@@zero_alloc strict]
+         val f : int -> int @@ portable [@@zero_alloc strict]
        The former provides a weaker "zero_alloc" guarantee than the latter.
 |}]
 
@@ -937,9 +939,11 @@ module type S_no_nrn = module type of M_nrn_for_mto
 
 [%%expect{|
 module M_assume_for_mto : sig val f : int -> int * int [@@zero_alloc] end
-module type S_no_assume = sig val f : int -> int * int [@@zero_alloc] end
+module type S_no_assume =
+  sig val f : int -> int * int @@ portable [@@zero_alloc] end
 module M_nrn_for_mto : sig val f : int -> int * int [@@zero_alloc] end
-module type S_no_nrn = sig val f : int -> int * int [@@zero_alloc] end
+module type S_no_nrn =
+  sig val f : int -> int * int @@ portable [@@zero_alloc] end
 |}]
 
 (**********************************************)
@@ -1047,8 +1051,8 @@ module type S = module type of M_infer2
 [%%expect{|
 module type S =
   sig
-    val f : 'a -> 'a [@@zero_alloc strict]
-    val g : 'a -> 'a [@@zero_alloc]
+    val f : 'a -> 'a @@ stateless [@@zero_alloc strict]
+    val g : 'a -> 'a @@ stateless [@@zero_alloc]
   end
 |}]
 
@@ -1127,7 +1131,10 @@ module type S = module type of M_explicit_arity_2
 [%%expect{|
 module M_explicit_arity_2 : sig type t = int -> int val f : int -> t end
 module type S =
-  sig type t = int -> int val f : int -> t [@@zero_alloc arity 2] end
+  sig
+    type t = int -> int
+    val f : int -> t @@ stateless [@@zero_alloc arity 2]
+  end
 |}]
 
 (***************************)
@@ -1146,7 +1153,7 @@ end
 module type S = module type of M_for_mto
 [%%expect{|
 module M_for_mto : sig val f : int -> int end
-module type S = sig val f : int -> int end
+module type S = sig val f : int -> int @@ portable end
 |}]
 
 (* [S] itself is fixed. *)
@@ -1157,11 +1164,11 @@ Line 1, characters 61-62:
                                                                  ^
 Error: Signature mismatch:
        Modules do not match:
-         sig val f : int -> int end
+         sig val f : int -> int @@ portable end
        is not included in
          sig val f : int -> int [@@zero_alloc] end
        Values do not match:
-         val f : int -> int
+         val f : int -> int @@ portable
        is not included in
          val f : int -> int [@@zero_alloc]
        The former provides a weaker "zero_alloc" guarantee than the latter.
@@ -1178,18 +1185,18 @@ module type S' = module type of M_for_mto
 module F' (X : S') : sig val[@zero_alloc] f : int -> int end = X
 module F (X : S) : sig val[@zero_alloc] f : int -> int end = X
 [%%expect{|
-module type S' = sig val f : int -> int [@@zero_alloc] end
+module type S' = sig val f : int -> int @@ portable [@@zero_alloc] end
 module F' : functor (X : S') -> sig val f : int -> int [@@zero_alloc] end
 Line 7, characters 61-62:
 7 | module F (X : S) : sig val[@zero_alloc] f : int -> int end = X
                                                                  ^
 Error: Signature mismatch:
        Modules do not match:
-         sig val f : int -> int end
+         sig val f : int -> int @@ portable end
        is not included in
          sig val f : int -> int [@@zero_alloc] end
        Values do not match:
-         val f : int -> int
+         val f : int -> int @@ portable
        is not included in
          val f : int -> int [@@zero_alloc]
        The former provides a weaker "zero_alloc" guarantee than the latter.

typing/typemod.ml

@@ -3562,11 +3562,9 @@ let type_module_type_of env smod =
   let mty = Mtype.scrape_for_type_of ~remove_aliases env tmty.mod_type in
   (* PR#5036: must not contain non-generalized type variables *)
   check_nongen_modtype env smod.pmod_loc mty;
-  (* for [module type of], we zap to identity modality for best legacy
-  compatibility *)
   let mty =
     remove_modality_and_zero_alloc_variables_mty env
-      ~zap_modality:Mode.Modality.Value.zap_to_id mty
+      ~zap_modality:Mode.Modality.Value.zap_to_floor mty
   in
   tmty, mty