Consider modalities when adding baggage to with-kinds

If a field has a constant modality, or a type is annotated with a constant
modality, then skip that type when adding it as baggage to the kind, both when
converting user-written kind annotations and inferring kinds on types.

The guts of this is a big, ugly pattern match on Jkind_axis and
Modes.Modality.Const.axis, which ideally can go away or get much simpler with a
refactor to unify these two types, but I decided to do it this way for now to
get something working that's known-correct, and refactor under green

testsuite/tests/parsetree/source_jane_street.ml

@@ -1071,25 +1071,16 @@ type 'a uncontended : immutable_data with 'a @@ uncontended
 type 'a uncontended_with_int : immutable_data with 'a @@ uncontended with int
 
 [%%expect{|
-type 'a list
-  : value mod local with 'a aliased with 'a many with 'a uncontended with 'a
-              portable with 'a internal with 'a
+type 'a list : value mod many with 'a uncontended with 'a portable with 'a
 type ('a, 'b) either
-  : value mod local with 'a * 'b aliased with 'a * 'b many with 'a * 'b
-              uncontended with 'a * 'b portable with 'a * 'b
-              internal with 'a * 'b
+  : value mod many with 'a * 'b uncontended with 'a * 'b
+              portable with 'a * 'b
 type 'a uncontended
-  : value mod local with 'a aliased with 'a many with 'a uncontended with 'a
-              portable with 'a internal with 'a
+  : value mod many with 'a uncontended with 'a portable with 'a
 type 'a uncontended_with_int
-  : value mod local with int
-'a aliased with int
-'a many with int
-'a
-              uncontended with int
+  : value mod many with int
+'a uncontended with int
 'a portable with int
-'a
-              internal with int
 'a
 |}]
 

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

@@ -1212,12 +1212,27 @@ type 'a t : value mod many = { x : 'a @@ many }
 type 'a t : value mod uncontended = { x : 'a @@ uncontended }
 type 'a t : value mod portable = { x : 'a @@ portable }
 [%%expect {|
-Line 1, characters 0-47:
-1 | type 'a t : value mod many = { x : 'a @@ many }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+type 'a t = { x : 'a @@ many; }
+Line 2, characters 0-61:
+2 | type 'a t : value mod uncontended = { x : 'a @@ uncontended }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "t" is immutable_data
          because it's a boxed record type.
-       But the kind of type "t" must be a subkind of value mod many
+       But the kind of type "t" must be a subkind of value mod uncontended
+         because of the annotation on the declaration of the type t.
+|}]
+(* CR layouts v2.8: this should be accepted *)
+
+type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many }
+type 'a t : immutable_data with 'a @@ uncontended = { x : 'a @@ uncontended }
+type 'a t : immutable_data with 'a @@ portable = { x : 'a @@ portable }
+[%%expect{|
+Line 1, characters 0-63:
+1 | type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "t" is immutable_data
+         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.
 |}]
 (* CR layouts v2.8: this should be accepted *)

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

@@ -0,0 +1,73 @@
+(* TEST
+    flags = "-extension layouts_alpha";
+    expect;
+*)
+let use_uncontended : 'a @ uncontended -> unit = fun _ -> ()
+let use_portable : 'a @ portable -> unit = fun _ -> ()
+let cross_uncontended : ('a : value mod uncontended) -> unit = fun _ -> ()
+type ('a : value mod uncontended) require_uncontended
+[%%expect{|
+val use_uncontended : ('a : value_or_null). 'a -> unit = <fun>
+val use_portable : ('a : value_or_null). 'a @ portable -> unit = <fun>
+val cross_uncontended : ('a : value mod uncontended). 'a -> unit = <fun>
+type ('a : value mod uncontended) require_uncontended
+|}]
+
+type 'a t = { contended : 'a @@ contended }
+[%%expect{|
+type 'a t = { contended : 'a @@ contended; }
+|}]
+
+type t_test = int t require_uncontended
+type t_test = int ref t require_uncontended
+[%%expect{|
+type t_test = int t require_uncontended
+type t_test = int ref t require_uncontended
+|}]
+
+let foo (t : int ref t @@ contended) = use_uncontended t
+[%%expect{|
+val foo : int ref t @ contended -> unit = <fun>
+|}]
+
+let foo (t : int ref t @@ contended) = use_uncontended t.contended
+[%%expect{|
+Line 1, characters 55-66:
+1 | let foo (t : int ref t @@ contended) = use_uncontended t.contended
+                                                           ^^^^^^^^^^^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : int ref t @@ contended) = cross_uncontended t
+[%%expect{|
+val foo : int ref t @ contended -> unit = <fun>
+|}]
+
+let foo (t : int t @@ nonportable) = use_portable t
+[%%expect{|
+val foo : int t -> unit = <fun>
+|}]
+
+let foo (t : _ t @@ nonportable) = use_portable t
+[%%expect{|
+Line 1, characters 48-49:
+1 | let foo (t : _ t @@ nonportable) = use_portable t
+                                                    ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many }
+type 'a t : immutable_data with 'a @@ uncontended = { x : 'a @@ uncontended }
+type 'a t : immutable_data with 'a @@ portable = { x : 'a @@ portable }
+[%%expect{|
+Line 1, characters 0-63:
+1 | type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "t" is
+         value mod many uncontended with 'a portable with 'a
+         because it's a boxed record type.
+       But the kind of type "t" must be a subkind of
+         value mod many uncontended with 'a portable with 'a
+         because of the annotation on the declaration of the type t.
+|}]
+(* CR layouts v2.8: this should be accepted *)

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

@@ -132,7 +132,7 @@ Error: This value escapes its region.
 
 (* ref *)
 type t : mutable_data = int ref
-type 'a t : mutable_data with 'a = 'a ref
+type 'a t : mutable_data with 'a @@ global many uncontended = 'a ref
 type ('a : mutable_data) t : mutable_data = 'a list
 [%%expect {|
 type t = int ref

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

@@ -154,7 +154,7 @@ Line 2, characters 15-16:
 Error: This value is "nonportable" but expected to be "portable".
 |}]
 
-let foo (t : ('a -> 'a) ref option @@ once) =
+let foo (t : ('a -> 'a ref) option @@ once) =
   use_many t
 
 [%%expect{|
@@ -426,7 +426,7 @@ Line 2, characters 15-16:
 Error: This value is "nonportable" but expected to be "portable".
 |}]
 
-let foo (t : ('a -> 'a) ref list @@ once) =
+let foo (t : ('a -> 'a ref) list @@ once) =
   use_many t
 
 [%%expect{|
@@ -919,52 +919,29 @@ module T : sig
 end = struct
   type 'a t = { x : 'a }
 end
-(* CR layouts v2.8: fix this *)
 [%%expect {|
-Lines 3-5, characters 6-3:
-3 | ......struct
-4 |   type 'a t = { x : 'a }
-5 | end
-Error: Signature mismatch:
-       Modules do not match:
-         sig type 'a t = { x : 'a; } end
-       is not included in
-         sig type 'a t : value mod uncontended end
-       Type declarations do not match:
-         type 'a t = { x : 'a; }
-       is not included in
-         type 'a t : value mod uncontended
-       The kind of the first is immutable_data
-         because of the definition of t at line 4, characters 2-24.
-       But the kind of the first must be a subkind of value mod uncontended
-         because of the definition of t at line 2, characters 2-43.
+module T : sig type 'a t : value mod uncontended end
 |}]
 
 let foo (t : int T.t @@ contended) = use_uncontended t
 [%%expect {|
-Line 1, characters 13-20:
-1 | let foo (t : int T.t @@ contended) = use_uncontended t
-                 ^^^^^^^
-Error: The type constructor "T.t" expects 0 argument(s),
-       but is here applied to 1 argument(s)
+val foo : int T.t @ contended -> unit = <fun>
 |}]
 
 let foo (t : _ T.t @@ contended) = use_uncontended t
 [%%expect {|
-Line 1, characters 13-18:
+Line 1, characters 51-52:
 1 | let foo (t : _ T.t @@ contended) = use_uncontended t
-                 ^^^^^
-Error: The type constructor "T.t" expects 0 argument(s),
-       but is here applied to 1 argument(s)
+                                                       ^
+Error: This value is "contended" but expected to be "uncontended".
 |}]
 
 let foo (t : int T.t @@ nonportable) = use_portable t
 [%%expect {|
-Line 1, characters 13-20:
+Line 1, characters 52-53:
 1 | let foo (t : int T.t @@ nonportable) = use_portable t
-                 ^^^^^^^
-Error: The type constructor "T.t" expects 0 argument(s),
-       but is here applied to 1 argument(s)
+                                                        ^
+Error: This value is "nonportable" but expected to be "portable".
 |}]
 
 (*************************)

testsuite/tests/typing-layouts-or-null/reexport.ml

@@ -22,8 +22,7 @@ Lines 2-4, characters 2-16:
 Error: The kind of type "'a or_null" is value_or_null
          because it is the primitive value_or_null type or_null.
        But the kind of type "'a or_null" must be a subkind of
-         value mod local with 'a aliased with 'a many with 'a
-                   uncontended with 'a portable with 'a internal with 'a
+         value mod many with 'a uncontended with 'a portable with 'a
          because of the definition of t at lines 2-4, characters 2-16.
 |}]
 

testsuite/tests/typing-layouts-products/basics_alpha.ml

@@ -68,8 +68,7 @@ Line 3, characters 0-39:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
          any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                  uncontended with t1
 t2 portable with t1
@@ -78,8 +77,7 @@ t2
 t2 non_null with t1
 t2
          & any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                    uncontended with t1
 t2 portable with t1
@@ -103,8 +101,7 @@ Line 3, characters 0-45:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
          any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                  uncontended with t1
 t2 portable with t1
@@ -113,8 +110,7 @@ t2
 t2 non_null with t1
 t2
          & any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                    uncontended with t1
 t2 portable with t1
@@ -139,8 +135,7 @@ Line 3, characters 0-62:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
          any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                  uncontended with t1
 t2 portable with t1
@@ -149,8 +144,7 @@ t2
 t2 non_null with t1
 t2
          & any mod global with t1
-t2 unique with t1
-t2 many with t1
+t2 unique many with t1
 t2
                    uncontended with t1
 t2 portable with t1

testsuite/tests/typing-modes/portable-contend.ml

@@ -365,8 +365,6 @@ val foo : int @ shared -> unit = <fun>
 module Iarray = Stdlib_stable.Iarray
 
 let foo (r @ contended) = Iarray.get r 42
-(* CR zqian: The following should pass; the modal kind system should mode cross
-iarray depending on the type of its element. *)
 [%%expect{|
 module Iarray = Stdlib_stable.Iarray
 Line 3, characters 37-38: