Modality.Value.Const should behave like a product (#3961)

Author: riaqn

testsuite/tests/typing-jkind-bounds/basics.ml

@@ -990,7 +990,7 @@ type ('a : immediate) t : value mod global = { mutable x : 'a }
 Line 1, characters 0-63:
 1 | type ('a : immediate) t : value mod global = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
@@ -1004,7 +1004,7 @@ type ('a : immediate) t : value mod aliased = { mutable x : 'a }
 Line 1, characters 0-64:
 1 | type ('a : immediate) t : value mod aliased = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod aliased
          because of the annotation on the declaration of the type t.
@@ -1018,7 +1018,7 @@ type ('a : immediate) t : value mod contended = { mutable x : 'a }
 Line 1, characters 0-66:
 1 | type ('a : immediate) t : value mod contended = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod contended
          because of the annotation on the declaration of the type t.
@@ -1032,7 +1032,7 @@ type ('a : immediate) t : value mod external_ = { mutable x : 'a }
 Line 1, characters 0-66:
 1 | type ('a : immediate) t : value mod external_ = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod external_
          because of the annotation on the declaration of the type t.
@@ -1046,7 +1046,7 @@ type ('a : immediate) t : value mod external64 = { mutable x : 'a }
 Line 1, characters 0-67:
 1 | type ('a : immediate) t : value mod external64 = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod external64
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-jkind-bounds/composite.ml

@@ -189,7 +189,7 @@ Line 1, characters 13-20:
 1 | let foo (t : int ref t @ contended) = use_uncontended t
                  ^^^^^^^
 Error: This type "int ref" should be an instance of type "('a : immutable_data)"
-       The kind of int ref is mutable_data with int @@ many unyielding.
+       The kind of int ref is mutable_data with int @@ unyielding many.
        But the kind of int ref must be a subkind of immutable_data
          because of the definition of t at line 1, characters 0-46.
 
@@ -341,7 +341,7 @@ Line 1, characters 13-20:
 1 | let foo (t : int ref t @ contended) = use_uncontended t
                  ^^^^^^^
 Error: This type "int ref" should be an instance of type "('a : immutable_data)"
-       The kind of int ref is mutable_data with int @@ many unyielding.
+       The kind of int ref is mutable_data with int @@ unyielding many.
        But the kind of int ref must be a subkind of immutable_data
          because of the definition of t at line 1, characters 0-73.
 

testsuite/tests/typing-jkind-bounds/predef.ml

@@ -176,7 +176,7 @@ type 'a t : mutable_data = 'a ref
 Line 1, characters 0-33:
 1 | type 'a t : mutable_data = 'a ref
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "'a ref" is mutable_data with 'a @@ many unyielding.
+Error: The kind of type "'a ref" is mutable_data with 'a @@ unyielding many.
        But the kind of type "'a ref" must be a subkind of mutable_data
          because of the definition of t at line 1, characters 0-33.
 
@@ -199,7 +199,7 @@ Line 1, characters 14-21:
                   ^^^^^^^
 Error: This type "int ref" should be an instance of type
          "('a : value mod portable)"
-       The kind of int ref is mutable_data with int @@ many unyielding.
+       The kind of int ref is mutable_data with int @@ unyielding many.
        But the kind of int ref must be a subkind of value mod portable
          because of the definition of require_portable at line 10, characters 0-47.
 
@@ -223,7 +223,7 @@ Line 1, characters 14-21:
                   ^^^^^^^
 Error: This type "int ref" should be an instance of type
          "('a : value mod contended)"
-       The kind of int ref is mutable_data with int @@ many unyielding.
+       The kind of int ref is mutable_data with int @@ unyielding many.
        But the kind of int ref must be a subkind of value mod contended
          because of the definition of require_contended at line 9, characters 0-49.
 

testsuite/tests/typing-jkind-bounds/printing.ml

@@ -179,7 +179,7 @@ Line 3, characters 11-12:
                ^
 Error: This type "a" = "int ref" should be an instance of type
          "('a : immutable_data)"
-       The kind of a is mutable_data with int @@ many unyielding.
+       The kind of a is mutable_data with int @@ unyielding many.
        But the kind of a must be a subkind of immutable_data
          because of the definition of t at line 2, characters 0-28.
 
@@ -343,15 +343,15 @@ Error: Signature mismatch:
        Modules do not match:
          sig type 'a t : mutable_data with 'a end
        is not included in
-         sig type 'a t : mutable_data with 'a @@ many unyielding end
+         sig type 'a t : mutable_data with 'a @@ unyielding many end
        Type declarations do not match:
          type 'a t : mutable_data with 'a
        is not included in
-         type 'a t : mutable_data with 'a @@ many unyielding
+         type 'a t : mutable_data with 'a @@ unyielding many
        The kind of the first is mutable_data with 'a
          because of the definition of t at line 4, characters 2-34.
        But the kind of the first must be a subkind of mutable_data
-         with 'a @@ many unyielding
+         with 'a @@ unyielding many
          because of the definition of t at line 2, characters 2-40.
 
        The first mode-crosses less than the second along:
@@ -423,14 +423,14 @@ Lines 3-5, characters 6-3:
 5 | end
 Error: Signature mismatch:
        Modules do not match:
-         sig type 'a t : mutable_data with 'a @@ many unyielding end
+         sig type 'a t : mutable_data with 'a @@ unyielding many end
        is not included in
          sig type 'a t : immutable_data with 'a end
        Type declarations do not match:
-         type 'a t : mutable_data with 'a @@ many unyielding
+         type 'a t : mutable_data with 'a @@ unyielding many
        is not included in
          type 'a t : immutable_data with 'a
-       The kind of the first is mutable_data with 'a @@ many unyielding
+       The kind of the first is mutable_data with 'a @@ unyielding many
          because of the definition of t at line 4, characters 2-40.
        But the kind of the first must be a subkind of immutable_data with 'a
          because of the definition of t at line 2, characters 2-56.

testsuite/tests/typing-jkind-bounds/records.ml

@@ -128,7 +128,7 @@ type 'a t : immutable_data = { mutable x : 'a }
 Line 1, characters 0-47:
 1 | type 'a t : immutable_data = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.
@@ -270,7 +270,7 @@ type 'a t : immutable_data with 'a = { mutable x : 'a }
 Line 1, characters 0-55:
 1 | type 'a t : immutable_data with 'a = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of immutable_data with 'a
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-jkind-bounds/subsumption/basics.ml

@@ -176,15 +176,15 @@ Error: Signature mismatch:
        Modules do not match:
          sig type 'a t : mutable_data with 'a end
        is not included in
-         sig type 'a t : mutable_data with 'a @@ many unyielding end
+         sig type 'a t : mutable_data with 'a @@ unyielding many end
        Type declarations do not match:
          type 'a t : mutable_data with 'a
        is not included in
-         type 'a t : mutable_data with 'a @@ many unyielding
+         type 'a t : mutable_data with 'a @@ unyielding many
        The kind of the first is mutable_data with 'a
          because of the definition of t at line 4, characters 2-34.
        But the kind of the first must be a subkind of mutable_data
-         with 'a @@ many unyielding
+         with 'a @@ unyielding many
          because of the definition of t at line 2, characters 2-40.
 
        The first mode-crosses less than the second along:
@@ -198,7 +198,7 @@ end = struct
   type 'a t : mutable_data with 'a @@ many unyielding
 end
 [%%expect {|
-module M : sig type 'a t : mutable_data with 'a @@ many unyielding end
+module M : sig type 'a t : mutable_data with 'a @@ unyielding many end
 |}]
 
 (* CR layouts v2.8: 'a u's kind should get normalized to just immutable_data *)

testsuite/tests/typing-jkind-bounds/subsumption/constraint.ml

@@ -141,7 +141,7 @@ Error: Signature mismatch:
          type 'a t = Foo of 'a constraint 'a = 'b ref
        is not included in
          type 'a t : immutable_data with 'b constraint 'a = 'b ref
-       The kind of the first is mutable_data with 'b @@ many unyielding
+       The kind of the first is mutable_data with 'b @@ unyielding many
          because of the definition of t at line 4, characters 2-46.
        But the kind of the first must be a subkind of immutable_data with 'b
          because of the definition of t at line 2, characters 2-59.

testsuite/tests/typing-jkind-bounds/subsumption/functors.ml

@@ -59,7 +59,7 @@ Line 4, characters 0-48:
 4 | type 'a t : immutable_data with 'a = 'a F(Ref).t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "'a F(Ref).t" is mutable_data
-         with 'a @@ many unyielding
+         with 'a @@ unyielding many
          because of the definition of t at line 2, characters 2-40.
        But the kind of type "'a F(Ref).t" must be a subkind of immutable_data
          with 'a
@@ -80,7 +80,7 @@ Line 4, characters 0-38:
 4 | type 'a t : mutable_data = 'a F(Ref).t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "'a F(Ref).t" is mutable_data
-         with 'a @@ many unyielding
+         with 'a @@ unyielding many
          because of the definition of t at line 2, characters 2-40.
        But the kind of type "'a F(Ref).t" must be a subkind of mutable_data
          because of the definition of t at line 4, characters 0-38.

testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml

@@ -367,6 +367,21 @@ end = struct
   type 'a t : immutable_data with 'a @@ portable contended portable
 end
 [%%expect {|
+Line 4, characters 40-48:
+4 |   type 'a t : immutable_data with 'a @@ portable contended portable
+                                            ^^^^^^^^
+Warning 213: This portability is overriden by portable later.
+
+Line 4, characters 40-48:
+4 |   type 'a t : immutable_data with 'a @@ portable contended portable
+                                            ^^^^^^^^
+Warning 213: This portability is overriden by portable later.
+
+Line 4, characters 40-48:
+4 |   type 'a t : immutable_data with 'a @@ portable contended portable
+                                            ^^^^^^^^
+Warning 213: This portability is overriden by portable later.
+
 module M : sig type 'a t : immutable_data with 'a @@ portable end
 |}]
 

testsuite/tests/typing-jkind-bounds/variants.ml

@@ -132,7 +132,7 @@ type 'a t : immutable_data = Foo of { mutable x : 'a }
 Line 1, characters 0-54:
 1 | type 'a t : immutable_data = Foo of { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.
@@ -274,7 +274,7 @@ type 'a t : immutable_data with 'a = Foo of { mutable x : 'a }
 Line 1, characters 0-62:
 1 | type 'a t : immutable_data with 'a = Foo of { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data with 'a @@ many unyielding
+Error: The kind of type "t" is mutable_data with 'a @@ unyielding many
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data with 'a
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-layouts/allow_any.ml

@@ -385,10 +385,10 @@ Lines 1-2, characters 0-34:
 Error: This variant or record definition does not match that of type "'a t"
        They have different unsafe mode crossing behavior:
        Both specify [@@unsafe_allow_any_mode_crossing], but their bounds are not equal
-         the original has: mod many portable unyielding stateless contended
-         immutable with 'a
-         but this has: mod many portable unyielding stateless contended
-         immutable
+         the original has: mod unyielding many stateless portable immutable
+         contended with 'a
+         but this has: mod unyielding many stateless portable immutable
+         contended
 |}]
 
 type ('a, 'b) arity_2 : immutable_data with 'b = { x : 'a }
@@ -406,10 +406,10 @@ Error: This variant or record definition does not match that of type
          "('a, 'b) arity_2"
        They have different unsafe mode crossing behavior:
        Both specify [@@unsafe_allow_any_mode_crossing], but their bounds are not equal
-         the original has: mod many portable unyielding stateless contended
-         immutable with 'b
-         but this has: mod many portable unyielding stateless contended
-         immutable with 'a
+         the original has: mod unyielding many stateless portable immutable
+         contended with 'b
+         but this has: mod unyielding many stateless portable immutable
+         contended with 'a
 |}]
 
 (* mcomp *)

testsuite/tests/typing-modal-kinds/basics.ml

@@ -934,7 +934,7 @@ Line 1, characters 10-19:
               ^^^^^^^^^
 Error: This type "int t ref" should be an instance of type
          "('a : value mod contended)"
-       The kind of int t ref is mutable_data with int t @@ many unyielding.
+       The kind of int t ref is mutable_data with int t @@ unyielding many.
        But the kind of int t ref must be a subkind of value mod contended
          because of the definition of require_contended at line 1, characters 0-49.
 

testsuite/tests/typing-modes/modes.ml

@@ -321,8 +321,12 @@ Error: Unrecognized modality foo.
 |}]
 
 type t = Foo of global_ string @@ global
-(* CR reduced-modality: this should warn. *)
 [%%expect{|
+Line 1, characters 16-23:
+1 | type t = Foo of global_ string @@ global
+                    ^^^^^^^
+Warning 213: This locality is overriden by global later.
+
 type t = Foo of global_ string
 |}]
 
@@ -346,8 +350,12 @@ Error: Unrecognized modality foo.
 type r = {
   global_ x : string @@ global
 }
-(* CR reduced-modality: this should warn. *)
 [%%expect{|
+Line 2, characters 2-9:
+2 |   global_ x : string @@ global
+      ^^^^^^^
+Warning 213: This locality is overriden by global later.
+
 type r = { global_ x : string; }
 |}]
 
@@ -369,8 +377,12 @@ type r = { x : string @@ global many aliased; }
 type r = {
   x : string @@ aliased global many aliased
 }
-(* CR reduced-modality: this should warn. *)
 [%%expect{|
+Line 2, characters 16-23:
+2 |   x : string @@ aliased global many aliased
+                    ^^^^^^^
+Warning 213: This uniqueness is overriden by aliased later.
+
 type r = { x : string @@ global many aliased; }
 |}]
 

testsuite/tests/typing-modes/mutable.ml

@@ -16,6 +16,54 @@ Line 2, characters 31-32:
 Error: This value escapes its region.
 |}]
 
+(* you can override those implied modalities *)
+type r = {mutable s : string @@ local}
+let foo (local_ s) = exclave_ {s}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+val foo : local_ string -> local_ r = <fun>
+|}]
+
+type r = {mutable s : string @@ global}
+[%%expect{|
+type r = { mutable s : string; }
+|}]
+
+type r = {mutable s : string @@ global yielding}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ yielding global}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ yielding}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ local yielding}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+|}]
+
+type r = {mutable s : string @@ yielding local}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+|}]
+
+type r = {mutable s : string @@ local unyielding}
+[%%expect{|
+type r = { mutable s : string @@ local unyielding; }
+|}]
+
+type r = {mutable s : string @@ unyielding local}
+[%%expect{|
+type r = { mutable s : string @@ local unyielding; }
+|}]
+
 (* [@no_mutable_implied_modalities] disables those implied modalities on the
    comonadic axes, and allows us to test [mutable] alone *)