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/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,75 @@
+(* 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 local with 'a many uncontended with 'a portable with 'a
+                   internal with 'a
+         because it's a boxed record type.
+       But the kind of type "t" must be a subkind of
+         value mod local with 'a many uncontended with 'a portable with 'a
+                   internal 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{|

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

@@ -365,14 +365,9 @@ 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:
-3 | let foo (r @ contended) = Iarray.get r 42
-                                         ^
-Error: This value is "contended" but expected to be "uncontended".
+val foo : 'a iarray @ contended -> 'a = <fun>
 |}]
 
 (* CR zqian: add portable/uncontended modality and test. *)

testsuite/tests/typing-signatures/nondep_regression.ml

@@ -13,5 +13,5 @@ module H = Make (struct type t end)
 [%%expect{|
 type 'a seq = 'a list
 module Make : functor (A : sig type t end) -> sig type t = A.t seq end
-module H : sig type t end
+module H : sig type t : value mod uncontended end
 |}]

typing/jkind.ml

@@ -616,15 +616,17 @@ module Bounds = struct
       }
       ~combine:Misc.Le_result.combine bounds1 bounds2
 
-  let add_baggage ~deep_only ~baggage bounds =
+  let add_baggage ~modality ~deep_only ~baggage bounds =
     (* Add the type as a baggage type along all deep axes *)
     Map.f
       { f =
           (fun ~axis (bound : _ Bound.t) : _ Bound.t ->
-            match deep_only, Axis.is_deep axis with
-            | false, _ | _, true ->
-              { bound with baggage = Baggage.add_baggage bound.baggage baggage }
-            | true, false -> bound)
+             if Jkind_axis.Axis.modality_is_const_for_axis axis modality
+             then bound
+             else (match (deep_only, Axis.is_deep axis) with
+               | false, _ | _, true ->
+                 { bound with baggage = Baggage.add_baggage bound.baggage baggage }
+               | true, false -> bound))
       }
       bounds
 
@@ -1080,15 +1082,15 @@ module Const = struct
       in
       jkind_of_product_annotations jkinds
     | With (base, type_, modalities) -> (
-      ignore modalities;  (* CR aspsmith: TODO *)
       let base = of_user_written_annotation_unchecked_level context base in
       match context with
       | Right_jkind _ -> raise ~loc:type_.ptyp_loc With_on_right
       | Left_jkind (transl_type, _) ->
         let type_ = transl_type type_ in
+        let modality = Typemode.transl_modalities ~maturity:Stable Immutable [] modalities in
         { layout = base.layout;
           upper_bounds =
-            Bounds.add_baggage ~deep_only:true ~baggage:type_ base.upper_bounds
+            Bounds.add_baggage ~modality ~deep_only:true ~baggage:type_ base.upper_bounds
         })
     | Default | Kind_of _ -> Misc.fatal_error "XXX unimplemented"
 
@@ -1196,9 +1198,9 @@ module Jkind_desc = struct
     in
     { to_ with upper_bounds }, added1 || added2
 
-  let add_baggage ~deep_only ~baggage t =
+  let add_baggage ~deep_only ~baggage ~modality t =
     { t with
-      upper_bounds = Bounds.add_baggage ~deep_only ~baggage t.upper_bounds
+      upper_bounds = Bounds.add_baggage ~deep_only ~baggage ~modality t.upper_bounds
     }
 
   let max = of_const Const.max
@@ -1255,7 +1257,7 @@ module Jkind_desc = struct
       let upper_bounds =
         List.fold_right
           (fun ty bounds ->
-            Bounds.add_baggage ~deep_only:false ~baggage:ty bounds)
+            Bounds.add_baggage ~deep_only:false ~baggage:ty bounds ~modality:Modality.Value.Const.id)
           tys
           (Bounds.min |> Bounds.disallow_right)
       in
@@ -1352,8 +1354,8 @@ end
 let add_nullability_crossing t =
   { t with jkind = Jkind_desc.add_nullability_crossing t.jkind }
 
-let add_baggage ~baggage t =
-  { t with jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage t.jkind }
+let add_baggage ?(modality=Mode.Modality.Value.Const.id) ~baggage t =
+  { t with jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage ~modality t.jkind }
 
 let has_baggage t = Bounds.has_baggage t.jkind.upper_bounds
 
@@ -1454,10 +1456,12 @@ let all_void_labels lbls =
 
 let add_labels_as_baggage lbls jkind =
   List.fold_right
-    (fun (lbl : Types.label_declaration) -> add_baggage ~baggage:lbl.ld_type)
+    (fun (lbl : Types.label_declaration) ->
+       add_baggage
+         ~baggage:lbl.ld_type
+         ~modality:lbl.ld_modalities)
     lbls jkind
 
-(* CR layouts v2.8: This should take modalities into account. *)
 let for_boxed_record lbls =
   if all_void_labels lbls
   then Builtin.immediate ~why:Empty_record
@@ -1469,7 +1473,7 @@ let for_boxed_record lbls =
     in
     add_labels_as_baggage lbls base
 
-(* CR layouts v2.8: This should take modalities into account. *)
+(* XCR layouts v2.8: This should take modalities into account. *)
 let for_unboxed_record ~jkind_of_type lbls =
   let open Types in
   let tys = List.map (fun lbl -> lbl.ld_type) lbls in
@@ -1527,7 +1531,8 @@ let for_boxed_variant cstrs =
         match cstr.cd_args with
         | Cstr_tuple args ->
           List.fold_right
-            (fun arg -> add_baggage ~baggage:arg.ca_type)
+            (fun arg ->
+               add_baggage ~modality:arg.ca_modalities ~baggage:arg.ca_type)
             args jkind
         | Cstr_record lbls -> add_labels_as_baggage lbls jkind
       in

typing/jkind.mli

@@ -324,8 +324,12 @@ end
 (** Take an existing [t] and add an ability to cross across the nullability axis. *)
 val add_nullability_crossing : 'd t -> 'd t
 
-(** Take an existing [t] and add some baggage. *)
-val add_baggage : baggage:Types.type_expr -> jkind_l -> jkind_l
+(** Take an existing [jkind_l] and add some baggage. *)
+val add_baggage :
+  ?modality:Mode.Modality.Value.Const.t ->
+  baggage:Types.type_expr ->
+  jkind_l ->
+  jkind_l
 
 (** Does this jkind have baggage? *)
 val has_baggage : jkind_l -> bool

typing/jkind_axis.ml

@@ -183,6 +183,58 @@ module Axis = struct
     | Modal Contention -> true
     | Nonmodal Externality -> true
     | Nonmodal Nullability -> false
+
+  (* CR aspsmith: This can get a lot simpler once we unify jkind axes with the axes in
+     Mode *)
+  let modality_is_const_for_axis (type a) (t : a t) modality = match t with
+    | Nonmodal Nullability | Nonmodal Externality -> false
+    | Modal axis ->
+      let atoms = Mode.Modality.Value.Const.to_list modality in
+      List.exists (fun (modality : Mode.Modality.t) ->
+        match (axis, modality) with
+        (* Constant modalities *)
+        | Locality, Atom (Comonadic Areality, Meet_with Global) -> true
+        | Linearity, Atom (Comonadic Linearity, Meet_with Many) -> true
+        | Uniqueness, Atom (Monadic Uniqueness, Join_with Unique) -> true
+        | Portability, Atom (Comonadic Portability, Meet_with Portable) -> true
+        | Contention, Atom (Monadic Contention, Join_with Contended) -> true
+        (* Modalities which are actually identity *)
+        | Locality, Atom (Comonadic Areality, Meet_with Local)
+        | Linearity, Atom (Comonadic Linearity, Meet_with Once)
+        | Uniqueness, Atom (Monadic Uniqueness, Join_with Aliased)
+        | Portability, Atom (Comonadic Portability, Meet_with Nonportable)
+        | Contention, Atom (Monadic Contention, Join_with Uncontended)
+          -> false
+        (* Modalities which are neither constant nor identiy *)
+        | Locality, Atom (Comonadic Areality, Meet_with Regional)
+        | Contention, Atom (Monadic Contention, Join_with Shared) ->
+          Misc.fatal_error
+            "Don't yet know how to interpret non-constant, non-identity modalities"
+        (* Modalities which join or meet on an illegal axis *)
+        | _, Atom (Comonadic _, Join_with _) | _, Atom (Monadic _, Meet_with _) ->
+          Misc.fatal_error "Illegal modality"
+        (* Mismatched axes *)
+        | Locality, Atom (Monadic Uniqueness, _)
+        | Locality, Atom (Monadic Contention, _)
+        | Locality, Atom (Comonadic Linearity, _)
+        | Locality, Atom (Comonadic Portability, _)
+        | Linearity, Atom (Comonadic Areality, _)
+        | Linearity, Atom (Monadic Uniqueness, _)
+        | Portability, Atom (Monadic Uniqueness, _)
+        | Contention, Atom (Monadic Uniqueness, _)
+        | Linearity, Atom (Comonadic Portability, _)
+        | Linearity, Atom (Monadic Contention, _)
+        | Uniqueness, Atom (Comonadic Areality, _)
+        | Uniqueness, Atom (Comonadic Linearity, _)
+        | Uniqueness, Atom (Comonadic Portability, _)
+        | Contention, Atom (Comonadic Areality, _)
+        | Contention, Atom (Comonadic Linearity, _)
+        | Contention, Atom (Comonadic Portability, _)
+        | Uniqueness, Atom (Monadic Contention, _)
+        | Portability, Atom (Comonadic Areality, _)
+        | Portability, Atom (Comonadic Linearity, _)
+        | Portability, Atom (Monadic Contention, _) -> false
+      ) atoms
 end
 
 module type Axed = sig

typing/jkind_axis.mli

@@ -68,6 +68,8 @@ module Axis : sig
   val name : _ t -> string
 
   val is_deep : _ t -> bool
+
+  val modality_is_const_for_axis : _ t -> Mode.Modality.Value.Const.t -> bool
 end
 
 (** [Axed] describes a type that is parameterized by axis. *)