diff --git a/jane/doc/extensions/uniqueness/intro.md b/jane/doc/extensions/uniqueness/intro.md
index 1ca9f3092a9..a1fae6156b6 100644
--- a/jane/doc/extensions/uniqueness/intro.md
+++ b/jane/doc/extensions/uniqueness/intro.md
@@ -76,9 +76,8 @@ type delayed_free = { id : int; callback : unit -> unit }
 let get_id : delayed_free @ once -> int @ many = fun t -> t.id
 ```
 
-We are working on a feature which will make it possible to use a value as `many`
-if its type prevents it from containing a function. For example, you will then
-be able to use an `int list @ once aliased` as `many` (but not as `unique`).
+This mode-crossing works through container types. For example, you can use an
+`int list @ once aliased` as `many` (but not as `unique`).
 
 ## Checking for Uniqueness
 
diff --git a/jane/doc/proposals/kind-inference.md b/jane/doc/proposals/kind-inference.md
index a7132869d70..19d5e9649c7 100644
--- a/jane/doc/proposals/kind-inference.md
+++ b/jane/doc/proposals/kind-inference.md
@@ -141,7 +141,7 @@ rec {
 q ::= best | not_best   (* quality of an inferred kind; best < not_best *)
 ```
 
-Mode crossing is not covered in this design. 
+Mode crossing is not covered in this design.
 
 However, it may be helpful to know that having e.g. `mod observing` in a kind
 means that `observing` is the upper bound for the locality mode of values whose
@@ -158,14 +158,14 @@ that kind.  Suppose `t : ... mod exclusive`. If a context requires `e` of type
 `exclusive` is sufficient. A requirement of `aliased` (the top mode) is
 completely unaffected.
 
-The key question: if `t : ... mod exclusive` and we have 
+The key question: if `t : ... mod exclusive` and we have
 `type ('a : ... mod aliased) t2`, is `t t2` valid? No! Even though
 `exclusive < aliased`. That's because `mod aliased` puts a *harder* requirement
 on its type (it must be agnostic between all of `unique`, `exclusive`, and
 `aliased`) than `mod exclusive` does (which says the type is agnostic between
 `unique` and `exclusive` only). This means that the subkind relation works
 backwards on monadic axes: `... mod aliased ≤ ... mod exclusive`. For this
-reason, in the presentation above, the monadic axis elements are listed in 
+reason, in the presentation above, the monadic axis elements are listed in
 reverse order: this document does not care about submoding or mode crossing
 directly, and writing the axes in reverse order gives us the right behavior
 on subkinding.
@@ -256,7 +256,7 @@ rec {
 Γ ⊢ jkind with field_types ↠ lay(χ); ⟪Ξ(χ) with types_for(Ξ, field_types)⟫
 ```
 
-In `K_OF`, we produce a kind in terms of `τ`, not just `κ`. This allows us
+In `KS_OF`, we produce a kind in terms of `τ`, not just `κ`. This allows us
 to make use of refinements to `τ` that we learn later, perhaps through
 functor application or GADT refinement.
 
diff --git a/otherlibs/dynlink/dune b/otherlibs/dynlink/dune
index fc5018604b8..eec16a3af2e 100644
--- a/otherlibs/dynlink/dune
+++ b/otherlibs/dynlink/dune
@@ -601,8 +601,8 @@
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Primitive.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Oprint.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Typemode.cmo
-  .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Btype.cmo
+  .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Subst.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Signature_with_global_bindings.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Bytesections.cmo
@@ -697,8 +697,8 @@
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Primitive.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Oprint.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Typemode.cmx
-  .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Btype.cmx
+  .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Subst.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Signature_with_global_bindings.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Bytesections.cmx
diff --git a/parsing/parser.mly b/parsing/parser.mly
index 4c60074d276..63afab52bfa 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -3964,6 +3964,7 @@ jkind_desc:
       in
       Mod ($1, modes)
     }
+  (* CR layouts v2.8: The types should be separated by AND, not WITH *)
   | jkind_annotation WITH core_type {
       With ($1, $3)
     }
diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli
index 74aba7388ed..90586701508 100644
--- a/parsing/parsetree.mli
+++ b/parsing/parsetree.mli
@@ -1296,6 +1296,8 @@ and module_binding =
 and jkind_annotation_desc =
   | Default
   | Abbreviation of string
+  (* CR layouts v2.8: [mod] can have only layouts on the left, not
+     full kind annotations. We may want to narrow this type some. *)
   | Mod of jkind_annotation * modes
   | With of jkind_annotation * core_type
   | Kind_of of core_type
diff --git a/testsuite/tests/typing-immediate/immediate.ml b/testsuite/tests/typing-immediate/immediate.ml
index 52309611352..2ffbb484fee 100644
--- a/testsuite/tests/typing-immediate/immediate.ml
+++ b/testsuite/tests/typing-immediate/immediate.ml
@@ -160,7 +160,7 @@ end;;
 Line 2, characters 2-41:
 2 |   type t = Foo of int | Bar [@@immediate]
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immediate
          because of the annotation on the declaration of the type t.
@@ -174,7 +174,7 @@ end;;
 Line 2, characters 2-38:
 2 |   type t = { foo : int } [@@immediate]
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 immediate
          because of the annotation on the declaration of the type t.
diff --git a/testsuite/tests/typing-layouts-or-null/reexport.ml b/testsuite/tests/typing-layouts-or-null/reexport.ml
index 96bd392eed7..9c58f5c49e9 100644
--- a/testsuite/tests/typing-layouts-or-null/reexport.ml
+++ b/testsuite/tests/typing-layouts-or-null/reexport.ml
@@ -21,7 +21,9 @@ Lines 2-4, characters 2-16:
 4 |     | This of 'a
 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
+       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
          because of the definition of t at lines 2-4, characters 2-16.
 |}]
 
diff --git a/testsuite/tests/typing-layouts/allow_illegal_crossing.ml b/testsuite/tests/typing-layouts/allow_illegal_crossing.ml
index 0da4bc8a58f..aff5d874aae 100644
--- a/testsuite/tests/typing-layouts/allow_illegal_crossing.ml
+++ b/testsuite/tests/typing-layouts/allow_illegal_crossing.ml
@@ -12,21 +12,35 @@ type a
 type b : value mod portable = { a : int; b : int }
 [%%expect {|
 type a
-type b : value mod portable = { a : int; b : int; }
+type b = { a : int; b : int; }
 |}]
 
 type a
 type b : value mod uncontended = Foo of int
 [%%expect {|
 type a
-type b : value mod uncontended = Foo of int
+type b = Foo of int
 |}]
 
 type a
 type b : value mod uncontended portable = Foo of int | Bar of int
 [%%expect {|
 type a
-type b : value mod uncontended portable = Foo of int | Bar of int
+type b = Foo of int | Bar of int
+|}]
+
+type a
+type b : value mod uncontended = Foo of int ref
+[%%expect {|
+type a
+type b : immutable_data = Foo of int ref
+|}]
+
+type a
+type b : value mod uncontended portable = Foo of int ref | Bar of (int -> int)
+[%%expect {|
+type a
+type b : immutable_data = Foo of int ref | Bar of (int -> int)
 |}]
 
 module _ = struct
@@ -45,50 +59,69 @@ Error: The kind of type "a" is value
 
 type t : value mod portable uncontended = { a : int; b : int }
 [%%expect {|
-type t : value mod uncontended portable = { a : int; b : int; }
+type t = { a : int; b : int; }
 |}]
 
 type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b }
 [%%expect {|
-type ('a, 'b) t : value mod uncontended portable = { a : 'a; b : 'b; }
+type ('a, 'b) t : immutable_data = { a : 'a; b : 'b; }
 |}]
 
 type t : value mod portable = private { foo : string }
 [%%expect {|
-type t : value mod portable = private { foo : string; }
+type t = private { foo : string; }
 |}]
 
 type a : value mod portable = { foo : string }
 type b : value mod portable = a = { foo : string }
 [%%expect {|
-type a : value mod portable = { foo : string; }
-type b = a : value mod portable = { foo : string; }
+type a = { foo : string; }
+type b = a = { foo : string; }
 |}]
 
 type a : value mod uncontended = private { foo : string }
 type b : value mod uncontended = a = private { foo : string }
 [%%expect {|
-type a : value mod uncontended = private { foo : string; }
-type b = a : value mod uncontended = private { foo : string; }
+type a = private { foo : string; }
+type b = a = private { foo : string; }
 |}]
 
 type t : value mod uncontended = private Foo of int | Bar
 [%%expect {|
-type t : value mod uncontended = private Foo of int | Bar
+type t = private Foo of int | Bar
 |}]
 
 type a : value mod uncontended = Foo of int | Bar
 type b : value mod uncontended = a = Foo of int | Bar
 [%%expect {|
-type a : value mod uncontended = Foo of int | Bar
-type b = a : value mod uncontended = Foo of int | Bar
+type a = Foo of int | Bar
+type b = a = Foo of int | Bar
 |}]
 
 type a : value mod portable = private Foo of int | Bar
 type b : value mod portable = a = private Foo of int | Bar
 [%%expect {|
-type a : value mod portable = private Foo of int | Bar
-type b = a : value mod portable = private Foo of int | Bar
+type a = private Foo of int | Bar
+type b = a = private Foo of int | Bar
+|}]
+
+type t : value mod uncontended = private Foo of int ref | Bar
+[%%expect {|
+type t : immutable_data = private Foo of int ref | Bar
+|}]
+
+type a : value mod uncontended = Foo of int ref | Bar
+type b : value mod uncontended = a = Foo of int ref | Bar
+[%%expect {|
+type a : immutable_data = Foo of int ref | Bar
+type b = a : immutable_data = Foo of int ref | Bar
+|}]
+
+type a : value mod portable = private Foo of (int -> int) | Bar
+type b : value mod portable = a = private Foo of (int -> int) | Bar
+[%%expect {|
+type a : immutable_data = private Foo of (int -> int) | Bar
+type b = a : immutable_data = private Foo of (int -> int) | Bar
 |}]
 
 module A : sig
@@ -97,7 +130,7 @@ end = struct
   type t = { a : string }
 end
 [%%expect {|
-module A : sig type t : value mod portable = { a : string; } end
+module A : sig type t = { a : string; } end
 |}]
 
 (********************************************)
@@ -107,7 +140,16 @@ type a : value mod portable uncontended = Foo of string
 type ('a : value mod portable uncontended) b
 type c = a b
 [%%expect {|
-type a : value mod uncontended portable = Foo of string
+type a = Foo of string
+type ('a : value mod uncontended portable) b
+type c = a b
+|}]
+
+type a : value mod portable uncontended = Foo of (string -> string)
+type ('a : value mod portable uncontended) b
+type c = a b
+[%%expect {|
+type a : immutable_data = Foo of (string -> string)
 type ('a : value mod uncontended portable) b
 type c = a b
 |}]
@@ -116,7 +158,7 @@ type t : value mod portable uncontended = { a : string; b : int }
 let f : ('a : value mod portable uncontended). 'a -> 'a = fun x -> x
 let g (x : t) = f x
 [%%expect {|
-type t : value mod uncontended portable = { a : string; b : int; }
+type t = { a : string; b : int; }
 val f : ('a : value mod uncontended portable). 'a -> 'a = <fun>
 val g : t -> t = <fun>
 |}]
@@ -124,21 +166,28 @@ val g : t -> t = <fun>
 type t : value mod portable uncontended = { a : int; b : int }
 let x : _ as (_ : value mod portable uncontended) = { a = 5; b = 5 }
 [%%expect {|
-type t : value mod uncontended portable = { a : int; b : int; }
+type t = { a : int; b : int; }
 val x : t = {a = 5; b = 5}
 |}]
 
 type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b }
 let x : _ as (_ : value mod portable uncontended) = { a = 5; b = 5 }
 [%%expect {|
-type ('a, 'b) t : value mod uncontended portable = { a : 'a; b : 'b; }
+type ('a, 'b) t : immutable_data = { a : 'a; b : 'b; }
 val x : (int, int) t = {a = 5; b = 5}
 |}]
 
 type t : value mod portable uncontended = Foo of string | Bar of int
 let x : _ as (_ : value mod portable uncontended) = Foo "hello world"
 [%%expect {|
-type t : value mod uncontended portable = Foo of string | Bar of int
+type t = Foo of string | Bar of int
+val x : t = Foo "hello world"
+|}]
+
+type t : value mod portable uncontended = Foo of string | Bar of (int -> int) ref
+let x : _ as (_ : value mod portable uncontended) = Foo "hello world"
+[%%expect {|
+type t : immutable_data = Foo of string | Bar of (int -> int) ref
 val x : t = Foo "hello world"
 |}]
 
@@ -151,7 +200,7 @@ type ('a : value mod portable) u = 'a
 type v = A.t u
 let x : _ as (_ : value mod portable) = ({ a = "hello" } : A.t)
 [%%expect {|
-module A : sig type t : value mod portable = { a : string; } end
+module A : sig type t = { a : string; } end
 type ('a : value mod portable) u = 'a
 type v = A.t u
 val x : A.t = {A.a = "hello"}
@@ -161,7 +210,7 @@ type t : value mod portable = { a : string }
 let my_str : string @@ nonportable = ""
 let y = ({ a = my_str } : t @@ portable)
 [%%expect {|
-type t : value mod portable = { a : string; }
+type t = { a : string; }
 val my_str : string = ""
 val y : t = {a = ""}
 |}]
@@ -170,7 +219,7 @@ type t : value mod portable = { a : string -> string }
 let my_fun @ nonportable = fun x -> x
 let y : t @@ portable = { a = my_fun }
 [%%expect {|
-type t : value mod portable = { a : string -> string; }
+type t : immutable_data = { a : string -> string; }
 val my_fun : 'a -> 'a = <fun>
 val y : t = {a = <fun>}
 |}]
@@ -181,7 +230,7 @@ let f () =
   let _ = ({ a = make_str () } : t @@ uncontended) in
   ()
 [%%expect {|
-type t : value mod uncontended = { a : string; }
+type t = { a : string; }
 val make_str : unit -> string = <fun>
 val f : unit -> unit = <fun>
 |}]
@@ -192,7 +241,7 @@ let f () =
   let _ : t @@ uncontended = { a = make_str () } in
   ()
 [%%expect {|
-type t : value mod uncontended = { a : string; }
+type t = { a : string; }
 val make_str : unit -> string = <fun>
 val f : unit -> unit = <fun>
 |}]
@@ -208,7 +257,7 @@ let f () =
   ()
 [%%expect {|
 type t_value
-type t : value mod uncontended portable = Foo of t_value
+type t : immutable_data = Foo of t_value
 val make_value : unit -> t_value = <fun>
 val f : unit -> unit = <fun>
 |}]
@@ -217,7 +266,7 @@ type t : value mod portable = { a : string -> string }
 let my_fun : _ @@ nonportable = fun x -> x
 let y = ({ a = my_fun } : _ @@ portable)
 [%%expect {|
-type t : value mod portable = { a : string -> string; }
+type t : immutable_data = { a : string -> string; }
 val my_fun : 'a -> 'a = <fun>
 Line 3, characters 15-21:
 3 | let y = ({ a = my_fun } : _ @@ portable)
@@ -233,7 +282,7 @@ type t : value mod portable uncontended = Foo of string | Bar of int
 let g (x : t @@ nonportable contended) = f x; f (Foo ""); f (Bar 10)
 [%%expect {|
 val f : 'a @ portable -> unit = <fun>
-type t : value mod uncontended portable = Foo of string | Bar of int
+type t = Foo of string | Bar of int
 val g : t @ contended -> unit = <fun>
 |}]
 
@@ -370,7 +419,7 @@ type t : value mod global = { a : int; b : int }
 Line 1, characters 0-48:
 1 | type t : value mod global = { a : int; b : int }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 global
          because of the annotation on the declaration of the type t.
@@ -381,7 +430,7 @@ type ('a, 'b) t : value mod many = { a : 'a; b : 'b }
 Line 1, characters 0-53:
 1 | type ('a, 'b) t : value mod many = { a : 'a; b : 'b }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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
          because of the annotation on the declaration of the type t.
@@ -460,21 +509,30 @@ end = struct
   type t = { a : string }
 end
 [%%expect {|
+module A : sig type t : value mod portable end
+|}]
+
+module A : sig
+  type t : value mod portable
+end = struct
+  type t = { a : string -> string }
+end
+[%%expect {|
 Lines 3-5, characters 6-3:
 3 | ......struct
-4 |   type t = { a : string }
+4 |   type t = { a : string -> string }
 5 | end
 Error: Signature mismatch:
        Modules do not match:
-         sig type t = { a : string; } end
+         sig type t = { a : string -> string; } end
        is not included in
          sig type t : value mod portable end
        Type declarations do not match:
-         type t = { a : string; }
+         type t = { a : string -> string; }
        is not included in
          type t : value mod portable
-       The kind of the first is value
-         because of the definition of t at line 4, characters 2-25.
+       The kind of the first is immutable_data
+         because of the definition of t at line 4, characters 2-35.
        But the kind of the first must be a subkind of value mod portable
          because of the definition of t at line 2, characters 2-29.
 |}]
@@ -487,16 +545,36 @@ end = struct
   type v = t u
 end
 [%%expect {|
+module A : sig type t = { a : string; } end
+|}, Principal{|
 Line 6, characters 11-12:
 6 |   type v = t u
                ^
 Error: This type "t" should be an instance of type "('a : value mod portable)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 4, characters 2-25.
        But the kind of t must be a subkind of value mod portable
          because of the definition of u at line 5, characters 2-39.
 |}]
 
+module A : sig
+  type t : value mod portable = { a : string -> string }
+end = struct
+  type t = { a : string -> string }
+  type ('a : value mod portable) u = 'a
+  type v = t u
+end
+[%%expect {|
+Line 6, characters 11-12:
+6 |   type v = t u
+               ^
+Error: This type "t" should be an instance of type "('a : value mod portable)"
+       The kind of t is immutable_data
+         because of the definition of t at line 4, characters 2-35.
+       But the kind of t must be a subkind of value mod portable
+         because of the definition of u at line 5, characters 2-39.
+|}]
+
 module A : sig
   type t : value mod portable = { a : string }
 end = struct
@@ -504,17 +582,37 @@ end = struct
   let x : _ as (_ : value mod portable) = { a = "hello" }
 end
 [%%expect {|
+module A : sig type t = { a : string; } end
+|}, Principal{|
 Line 5, characters 42-57:
 5 |   let x : _ as (_ : value mod portable) = { a = "hello" }
                                               ^^^^^^^^^^^^^^^
 Error: This expression has type "t" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 4, characters 2-25.
        But the kind of t must be a subkind of value mod portable
          because of the annotation on the wildcard _ at line 5, characters 20-38.
 |}]
 
+module A : sig
+  type t : value mod portable = { a : string -> string }
+end = struct
+  type t = { a : string -> string }
+  let x : _ as (_ : value mod portable) = { a = fun _ -> "hello" }
+end
+[%%expect {|
+Line 5, characters 42-66:
+5 |   let x : _ as (_ : value mod portable) = { a = fun _ -> "hello" }
+                                              ^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This expression has type "t" but an expression was expected of type
+         "('a : value mod portable)"
+       The kind of t is immutable_data
+         because of the definition of t at line 4, characters 2-35.
+       But the kind of t must be a subkind of value mod portable
+         because of the annotation on the wildcard _ at line 5, characters 20-38.
+|}]
+
 type a
 type b : value mod portable = a
 [%%expect {|
@@ -532,11 +630,18 @@ type a = { foo : int; bar : string }
 type b : any mod portable = a
 [%%expect {|
 type a = { foo : int; bar : string; }
+type b = a
+|}]
+
+type a = { foo : int -> int; bar : string }
+type b : any mod portable = a
+[%%expect {|
+type a = { foo : int -> int; bar : string; }
 Line 2, characters 0-29:
 2 | type b : any mod portable = a
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-36.
+Error: The kind of type "a" is immutable_data
+         because of the definition of a at line 1, characters 0-43.
        But the kind of type "a" must be a subkind of any mod portable
          because of the definition of b at line 2, characters 0-29.
 |}]
@@ -545,11 +650,18 @@ type a = Foo of int | Bar of string
 type b : any mod uncontended = a
 [%%expect {|
 type a = Foo of int | Bar of string
+type b = a
+|}]
+
+type a = Foo of int ref | Bar of string
+type b : any mod uncontended = a
+[%%expect {|
+type a = Foo of int ref | Bar of string
 Line 2, characters 0-32:
 2 | type b : any mod uncontended = a
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-35.
+Error: The kind of type "a" is immutable_data
+         because of the definition of a at line 1, characters 0-39.
        But the kind of type "a" must be a subkind of any mod uncontended
          because of the definition of b at line 2, characters 0-32.
 |}]
@@ -575,51 +687,79 @@ type a = { foo : string }
 type b : value mod portable = a = { foo : string }
 [%%expect {|
 type a = { foo : string; }
-Line 2, characters 0-50:
-2 | type b : value mod portable = a = { foo : string }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-25.
-       But the kind of type "a" must be a subkind of value mod portable
-         because of the definition of b at line 2, characters 0-50.
+type b = a = { foo : string; }
 |}]
 
 type a = private { foo : string }
 type b : value mod uncontended = a = private { foo : string }
 [%%expect {|
 type a = private { foo : string; }
-Line 2, characters 0-61:
-2 | type b : value mod uncontended = a = private { foo : string }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-33.
-       But the kind of type "a" must be a subkind of value mod uncontended
-         because of the definition of b at line 2, characters 0-61.
+type b = a = private { foo : string; }
+|}]
+
+type a = { foo : string -> string }
+type b : value mod portable = a = { foo : string -> string }
+[%%expect {|
+type a = { foo : string -> string; }
+Line 2, characters 0-60:
+2 | type b : value mod portable = a = { foo : string -> string }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "a" is immutable_data
+         because of the definition of a at line 1, characters 0-35.
+       But the kind of type "a" must be a subkind of immutable_data
+         because of the definition of b at line 2, characters 0-60.
+|}]
+
+type a = private { foo : int array }
+type b : value mod uncontended = a = private { foo : int array }
+[%%expect {|
+type a = private { foo : int array; }
+Line 2, characters 0-64:
+2 | type b : value mod uncontended = a = private { foo : int array }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "a" is immutable_data
+         because of the definition of a at line 1, characters 0-36.
+       But the kind of type "a" must be a subkind of immutable_data
+         because of the definition of b at line 2, characters 0-64.
 |}]
 
 type a = Foo of string | Bar
 type b : value mod uncontended = a = Foo of string | Bar
 [%%expect {|
 type a = Foo of string | Bar
+type b = a = Foo of string | Bar
+|}]
+
+type a = private Foo of string | Bar
+type b : value mod portable = a = private Foo of string | Bar
+[%%expect {|
+type a = private Foo of string | Bar
+type b = a = private Foo of string | Bar
+|}]
+
+type a = Foo of { mutable x : int } | Bar
+type b : value mod uncontended = a = Foo of string | Bar
+[%%expect {|
+type a = Foo of { mutable x : int; } | Bar
 Line 2, characters 0-56:
 2 | type b : value mod uncontended = a = Foo of string | Bar
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-28.
-       But the kind of type "a" must be a subkind of value mod uncontended
+Error: The kind of type "a" is mutable_data
+         because of the definition of a at line 1, characters 0-41.
+       But the kind of type "a" must be a subkind of immutable_data
          because of the definition of b at line 2, characters 0-56.
 |}]
 
-type a = private Foo of string | Bar
+type a = private Foo of (int -> int) | Bar
 type b : value mod portable = a = private Foo of string | Bar
 [%%expect {|
-type a = private Foo of string | Bar
+type a = private Foo of (int -> int) | Bar
 Line 2, characters 0-61:
 2 | type b : value mod portable = a = private Foo of string | Bar
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "a" is value
-         because of the definition of a at line 1, characters 0-36.
-       But the kind of type "a" must be a subkind of value mod portable
+Error: The kind of type "a" is immutable_data
+         because of the definition of a at line 1, characters 0-42.
+       But the kind of type "a" must be a subkind of immutable_data
          because of the definition of b at line 2, characters 0-61.
 |}]
 
@@ -644,16 +784,36 @@ type u = t of_portable
 [%%expect {|
 type ('a : value mod portable) of_portable
 type t = { foo : int; }
+type u = t of_portable
+|}, Principal{|
+type ('a : value mod portable) of_portable
+type t = { foo : int; }
 Line 3, characters 9-10:
 3 | type u = t of_portable
              ^
 Error: This type "t" should be an instance of type "('a : value mod portable)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 2, characters 0-22.
        But the kind of t must be a subkind of value mod portable
          because of the definition of of_portable at line 1, characters 0-42.
 |}]
 
+type ('a : value mod portable) of_portable
+type t = { foo : int -> int }
+type u = t of_portable
+[%%expect {|
+type ('a : value mod portable) of_portable
+type t = { foo : int -> int; }
+Line 3, characters 9-10:
+3 | type u = t of_portable
+             ^
+Error: This type "t" should be an instance of type "('a : value mod portable)"
+       The kind of t is immutable_data
+         because of the definition of t at line 2, characters 0-29.
+       But the kind of t must be a subkind of value mod portable
+         because of the definition of of_portable at line 1, characters 0-42.
+|}]
+
 let f : ('a : value mod portable). 'a -> 'a = fun x -> x
 let _ = f (fun x -> x)
 [%%expect {|
@@ -677,7 +837,7 @@ Line 2, characters 10-18:
               ^^^^^^^^
 Error: This expression has type "int ref"
        but an expression was expected of type "('a : value mod uncontended)"
-       The kind of int ref is value.
+       The kind of int ref is mutable_data.
        But the kind of int ref must be a subkind of value mod uncontended
          because of the definition of f at line 1, characters 4-5.
 |}]
@@ -727,7 +887,7 @@ Line 2, characters 45-61:
                                                  ^^^^^^^^^^^^^^^^
 Error: This expression has type "t" but an expression was expected of type
          "('a : value mod uncontended)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 1, characters 0-24.
        But the kind of t must be a subkind of value mod uncontended
          because of the annotation on the wildcard _ at line 2, characters 20-41.
@@ -742,7 +902,7 @@ Line 2, characters 55-67:
                                                            ^^^^^^^^^^^^
 Error: This expression has type "t" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 1, characters 0-23.
        But the kind of t must be a subkind of value mod portable
          because of the annotation on the universal variable 'a.
diff --git a/testsuite/tests/typing-layouts/annots.ml b/testsuite/tests/typing-layouts/annots.ml
index d70a26eec59..148eebad05d 100644
--- a/testsuite/tests/typing-layouts/annots.ml
+++ b/testsuite/tests/typing-layouts/annots.ml
@@ -250,7 +250,7 @@ Line 1, characters 21-23:
                          ^^
 Error: This alias is bound to type "int list"
        but is used as an instance of type "('a : immediate)"
-       The kind of int list is value
+       The kind of int list is immutable_data
          because it's a boxed variant type.
        But the kind of int list must be a subkind of immediate
          because of the annotation on the type variable 'a.
@@ -264,7 +264,7 @@ Line 1, characters 21-23:
                          ^^
 Error: This alias is bound to type "int list"
        but is used as an instance of type "('a : value mod global)"
-       The kind of int list is value
+       The kind of int list is immutable_data
          because it's a boxed variant type.
        But the kind of int list must be a subkind of value mod global
          because of the annotation on the type variable 'a.
@@ -1083,7 +1083,7 @@ type t : value mod global = { x : int}
 Line 1, characters 0-38:
 1 | type t : value mod global = { x : int}
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 global
          because of the annotation on the declaration of the type t.
@@ -1091,16 +1091,8 @@ Error: The kind of type "t" is value
 
 type t : any mod portable = { x : float }
 [%%expect {|
-Line 1, characters 0-41:
-1 | type t : any mod portable = { x : float }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed record type.
-       But the kind of type "t" must be a subkind of any mod portable
-         because of the annotation on the declaration of the type t.
+type t = { x : float; }
 |}]
-(* CR layouts v2.8: This should be accepted, because t should be inferred to
-   mode-cross portability. *)
 
 type t = { x : int } [@@unboxed]
 let f (x : t) : _ as (_ : immediate) = x
@@ -1128,7 +1120,7 @@ type t : value mod global = { x : t_value }
 Line 1, characters 0-43:
 1 | type t : value mod global = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 global
          because of the annotation on the declaration of the type t.
@@ -1139,7 +1131,7 @@ type t : value mod unique = { x : t_value }
 Line 1, characters 0-43:
 1 | type t : value mod unique = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 unique
          because of the annotation on the declaration of the type t.
@@ -1150,7 +1142,7 @@ type t : value mod many = { x : t_value }
 Line 1, characters 0-41:
 1 | type t : value mod many = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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
          because of the annotation on the declaration of the type t.
@@ -1161,7 +1153,7 @@ type t : value mod portable = { x : t_value }
 Line 1, characters 0-45:
 1 | type t : value mod portable = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 portable
          because of the annotation on the declaration of the type t.
@@ -1172,7 +1164,7 @@ type t : value mod uncontended = { x : t_value }
 Line 1, characters 0-48:
 1 | type t : value mod uncontended = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 uncontended
          because of the annotation on the declaration of the type t.
@@ -1183,7 +1175,7 @@ type t : value mod external_ = { x : t_value }
 Line 1, characters 0-46:
 1 | type t : value mod external_ = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 external_
          because of the annotation on the declaration of the type t.
@@ -1209,7 +1201,7 @@ type t : value mod global = Foo of int
 Line 1, characters 0-38:
 1 | type t : value mod global = Foo of int
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant 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.
@@ -1217,13 +1209,7 @@ Error: The kind of type "t" is value
 
 type t : any mod portable = Foo of float
 [%%expect {|
-Line 1, characters 0-40:
-1 | type t : any mod portable = Foo of float
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed variant type.
-       But the kind of type "t" must be a subkind of any mod portable
-         because of the annotation on the declaration of the type t.
+type t = Foo of float
 |}]
 
 type t = Foo | Bar
@@ -1273,7 +1259,7 @@ type t : value mod global = Foo of t_value
 Line 1, characters 0-42:
 1 | type t : value mod global = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant 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.
@@ -1284,7 +1270,7 @@ type t : value mod unique = Foo of t_value
 Line 1, characters 0-42:
 1 | type t : value mod unique = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod unique
          because of the annotation on the declaration of the type t.
@@ -1295,7 +1281,7 @@ type t : value mod many = Foo of t_value
 Line 1, characters 0-40:
 1 | type t : value mod many = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod many
          because of the annotation on the declaration of the type t.
@@ -1306,7 +1292,7 @@ type t : value mod portable = Foo of t_value
 Line 1, characters 0-44:
 1 | type t : value mod portable = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod portable
          because of the annotation on the declaration of the type t.
@@ -1317,7 +1303,7 @@ type t : value mod uncontended = Foo of t_value
 Line 1, characters 0-47:
 1 | type t : value mod uncontended = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        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.
@@ -1328,7 +1314,7 @@ type t : value mod external_ = Foo of t_value
 Line 1, characters 0-45:
 1 | type t : value mod external_ = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant 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.
diff --git a/testsuite/tests/typing-layouts/jkinds.ml b/testsuite/tests/typing-layouts/jkinds.ml
index ef60dc46956..fb301d62ca4 100644
--- a/testsuite/tests/typing-layouts/jkinds.ml
+++ b/testsuite/tests/typing-layouts/jkinds.ml
@@ -3,23 +3,19 @@
  expect;
 *)
 
-(********************************)
-(* Test 1: Unimplemented syntax *)
+(******************)
+(* Test 1: Syntax *)
 
 type 'a list : immutable_data with 'a
 
 [%%expect{|
->> Fatal error: XXX unimplemented
-Uncaught exception: Misc.Fatal_error
-
+type 'a list : immutable_data
 |}]
 
 type ('a, 'b) either : immutable_data with 'a * 'b
 
 [%%expect{|
->> Fatal error: XXX unimplemented
-Uncaught exception: Misc.Fatal_error
-
+type ('a, 'b) either : immutable_data
 |}]
 
 type 'a gel : kind_of_ 'a mod global
@@ -721,7 +717,7 @@ type t : any mod global = { x : string }
 Line 1, characters 0-40:
 1 | type t : any mod global = { x : string }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod global
          because of the annotation on the declaration of the type t.
@@ -732,7 +728,7 @@ type t : any mod unique = { x : string }
 Line 1, characters 0-40:
 1 | type t : any mod unique = { x : string }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod unique
          because of the annotation on the declaration of the type t.
@@ -743,7 +739,7 @@ type t : any mod external_ = { x : string }
 Line 1, characters 0-43:
 1 | type t : any mod external_ = { x : string }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod external_
          because of the annotation on the declaration of the type t.
@@ -753,22 +749,17 @@ type t : any mod many = { x : string }
 type t : any mod portable = { x : string }
 type t : any mod uncontended = { x : string }
 [%%expect {|
-Line 1, characters 0-38:
-1 | type t : any mod many = { x : string }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed record type.
-       But the kind of type "t" must be a subkind of any mod many
-         because of the annotation on the declaration of the type t.
+type t = { x : string; }
+type t = { x : string; }
+type t = { x : string; }
 |}]
-(* CR layouts v2.8: This should be accepted *)
 
 type t : any mod many = { x : t_value }
 [%%expect{|
 Line 1, characters 0-39:
 1 | type t : any mod many = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod many
          because of the annotation on the declaration of the type t.
@@ -779,7 +770,7 @@ type t : any mod uncontended = { x : t_value }
 Line 1, characters 0-46:
 1 | type t : any mod uncontended = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod uncontended
          because of the annotation on the declaration of the type t.
@@ -790,7 +781,7 @@ type t : any mod portable = { x : t_value }
 Line 1, characters 0-43:
 1 | type t : any mod portable = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod portable
          because of the annotation on the declaration of the type t.
@@ -801,7 +792,7 @@ type t : any mod many uncontended portable global = { x : t_value }
 Line 1, characters 0-67:
 1 | type t : any mod many uncontended portable global = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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
          any mod global many uncontended portable
@@ -812,15 +803,8 @@ type u : immediate
 type t : value mod portable many uncontended = { x : string; y : int; z : u }
 [%%expect {|
 type u : immediate
-Line 2, characters 0-77:
-2 | type t : value mod portable many uncontended = { x : string; y : int; z : u }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         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.
+type t = { x : string; y : int; z : u; }
 |}]
-(* CR layouts v2.8: This should be accepted *)
 
 type t = { x : string }
 let foo : _ as (_ : value mod external_) = { x = "string" }
@@ -831,7 +815,7 @@ Line 2, characters 43-59:
                                                ^^^^^^^^^^^^^^^^
 Error: This expression has type "t" but an expression was expected of type
          "('a : value mod external_)"
-       The kind of t is value
+       The kind of t is immutable_data
          because of the definition of t at line 1, characters 0-23.
        But the kind of t must be a subkind of value mod external_
          because of the annotation on the wildcard _ at line 2, characters 20-39.
@@ -841,22 +825,17 @@ type t : any mod uncontended = { x : int }
 type t : any mod portable = { x : int }
 type t : any mod many = { x : int }
 [%%expect{|
-Line 1, characters 0-42:
-1 | type t : any mod uncontended = { x : int }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed record type.
-       But the kind of type "t" must be a subkind of any mod uncontended
-         because of the annotation on the declaration of the type t.
+type t = { x : int; }
+type t = { x : int; }
+type t = { x : int; }
 |}]
-(* CR layouts v2.8: this should be accepted *)
 
 type t : any mod global = { x : int }
 [%%expect {|
 Line 1, characters 0-37:
 1 | type t : any mod global = { x : int }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod global
          because of the annotation on the declaration of the type t.
@@ -867,7 +846,7 @@ type t : any mod external_ = { x : int }
 Line 1, characters 0-40:
 1 | type t : any mod external_ = { x : int }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod external_
          because of the annotation on the declaration of the type t.
@@ -878,7 +857,7 @@ type t : any mod unique = { x : int }
 Line 1, characters 0-37:
 1 | type t : any mod unique = { x : int }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 any mod unique
          because of the annotation on the declaration of the type t.
@@ -1000,22 +979,15 @@ val v : int = 5
 
 type ('a : immediate) t : value mod many portable = { mutable x : 'a }
 [%%expect {|
-Line 1, characters 0-70:
-1 | type ('a : immediate) t : value mod many portable = { mutable x : 'a }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed record type.
-       But the kind of type "t" must be a subkind of mutable_data
-         because of the annotation on the declaration of the type t.
+type ('a : immediate) t = { mutable x : 'a; }
 |}]
-(* CR layouts v2.8: this should be accepted *)
 
 type ('a : immediate) t : value mod global = { mutable x : 'a }
 [%%expect {|
 Line 1, characters 0-63:
 1 | type ('a : immediate) t : value mod global = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is mutable_data
          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.
@@ -1026,7 +998,7 @@ type ('a : immediate) t : value mod unique = { mutable x : 'a }
 Line 1, characters 0-63:
 1 | type ('a : immediate) t : value mod unique = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is mutable_data
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod unique
          because of the annotation on the declaration of the type t.
@@ -1037,7 +1009,7 @@ type ('a : immediate) t : value mod uncontended = { mutable x : 'a }
 Line 1, characters 0-68:
 1 | type ('a : immediate) t : value mod uncontended = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is mutable_data
          because it's a boxed record type.
        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.
@@ -1048,7 +1020,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 value
+Error: The kind of type "t" is mutable_data
          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.
@@ -1059,7 +1031,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 value
+Error: The kind of type "t" is mutable_data
          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.
@@ -1082,28 +1054,22 @@ type t = Foo | Bar
 type t = Foo | Bar
 type t = Foo | Bar
 |}]
-(* CR layouts v2.8: These outputs should include kinds *)
 
 type t : any mod uncontended = Foo of int | Bar
 type t : any mod portable = Foo of int | Bar
 type t : any mod many = Foo of int | Bar
 [%%expect {|
-Line 1, characters 0-47:
-1 | type t : any mod uncontended = Foo of int | Bar
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
-         because it's a boxed variant type.
-       But the kind of type "t" must be a subkind of any mod uncontended
-         because of the annotation on the declaration of the type t.
+type t = Foo of int | Bar
+type t = Foo of int | Bar
+type t = Foo of int | Bar
 |}]
-(* CR layouts v2.8: this should be accepted *)
 
 type t : any mod unique = Foo of int | Bar
 [%%expect {|
 Line 1, characters 0-42:
 1 | type t : any mod unique = Foo of int | Bar
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of any mod unique
          because of the annotation on the declaration of the type t.
@@ -1114,7 +1080,7 @@ type t : any mod global = Foo of int | Bar
 Line 1, characters 0-42:
 1 | type t : any mod global = Foo of int | Bar
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of any mod global
          because of the annotation on the declaration of the type t.
@@ -1126,7 +1092,7 @@ type t : any mod external_ = Foo of int | Bar
 Line 1, characters 0-45:
 1 | type t : any mod external_ = Foo of int | Bar
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of any mod external_
          because of the annotation on the declaration of the type t.
@@ -1249,7 +1215,7 @@ type 'a t : value mod portable = { x : 'a @@ portable }
 Line 1, characters 0-47:
 1 | type 'a t : value mod many = { x : 'a @@ many }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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
          because of the annotation on the declaration of the type t.
@@ -1261,7 +1227,7 @@ type 'a t : value mod unique = { x : 'a @@ unique }
 Line 1, characters 0-51:
 1 | type 'a t : value mod unique = { x : 'a @@ unique }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 unique
          because of the annotation on the declaration of the type t.
@@ -1272,7 +1238,7 @@ type 'a t : value mod global = { x : 'a @@ global }
 Line 1, characters 0-51:
 1 | type 'a t : value mod global = { x : 'a @@ global }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 global
          because of the annotation on the declaration of the type t.
@@ -1574,7 +1540,7 @@ type 'a t : value mod global = { x : 'a }
 Line 1, characters 0-41:
 1 | type 'a t : value mod global = { x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 global
          because of the annotation on the declaration of the type t.
@@ -1585,8 +1551,22 @@ type 'a t : value mod many = { x : 'a }
 Line 1, characters 0-39:
 1 | type 'a t : value mod many = { x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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
          because of the annotation on the declaration of the type t.
 |}]
+
+(*************************************)
+(* Test 12: Bug in check_constraints *)
+
+(* This requires the [Ctype.instance] call in [check_constraints_rec]. *)
+type 'a u
+type 'a t =
+  | None
+  | Some of ('a * 'a) t u
+
+[%%expect{|
+type 'a u
+type 'a t = None | Some of ('a * 'a) t u
+|}]
diff --git a/testsuite/tests/typing-layouts/modules.ml b/testsuite/tests/typing-layouts/modules.ml
index 5d736b34cbc..4da024afa5c 100644
--- a/testsuite/tests/typing-layouts/modules.ml
+++ b/testsuite/tests/typing-layouts/modules.ml
@@ -340,10 +340,11 @@ type ('a : value) t4_val
 type t4 = M4.s t4_val;;
 [%%expect {|
 module F4 : functor (X : sig type t end) -> sig type s = Foo of X.t end
-module M4 : sig type s end
+module M4 : sig type s : immutable_data end
 type 'a t4_val
 type t4 = M4.s t4_val
 |}]
+(* CR layouts v2.8: The appearance of [immutable_data] there is just wrong. *)
 
 type ('a : float64) t4_float64
 type t4f' = M4.s t4_float64;;
diff --git a/testsuite/tests/typing-layouts/modules_alpha.ml b/testsuite/tests/typing-layouts/modules_alpha.ml
index 8f7e69885e0..766f93a8138 100644
--- a/testsuite/tests/typing-layouts/modules_alpha.ml
+++ b/testsuite/tests/typing-layouts/modules_alpha.ml
@@ -283,11 +283,12 @@ type ('a : void) t4_void
 type t4 = M4.s t4_val;;
 [%%expect {|
 module F4 : functor (X : sig type t end) -> sig type s = Foo of X.t end
-module M4 : sig type s end
+module M4 : sig type s : immutable_data end
 type 'a t4_val
 type ('a : void) t4_void
 type t4 = M4.s t4_val
 |}]
+(* CR layouts v2.8: The appearance of [immutable_data] there is just wrong. *)
 
 type t4' = M4.s t4_void;;
 [%%expect {|
diff --git a/testsuite/tests/typing-layouts/with.ml b/testsuite/tests/typing-layouts/with.ml
new file mode 100644
index 00000000000..23ebcbf563f
--- /dev/null
+++ b/testsuite/tests/typing-layouts/with.ml
@@ -0,0 +1,574 @@
+(* TEST
+    expect;
+*)
+
+let use_global : 'a @ global -> unit = fun _ -> ()
+let use_unique : 'a @ unique -> unit = fun _ -> ()
+let use_uncontended : 'a @ uncontended -> unit = fun _ -> ()
+let use_portable : 'a @ portable -> unit = fun _ -> ()
+let use_many : 'a @ many -> unit = fun _ -> ()
+[%%expect{|
+val use_global : 'a -> unit = <fun>
+val use_unique : 'a @ unique -> unit = <fun>
+val use_uncontended : 'a -> unit = <fun>
+val use_portable : 'a @ portable -> unit = <fun>
+val use_many : 'a -> unit = <fun>
+|}]
+
+(************************************************)
+(* TEST 1: Mode crossing looks through [option] *)
+
+let foo (t : int option @@ contended nonportable once) =
+    use_uncontended t;
+    use_portable t;
+    use_many t
+[%%expect{|
+val foo : int option @ once contended -> unit = <fun>
+|}]
+
+let foo (t : int option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : int option @@ aliased) =
+  use_unique t;
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t;
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* crosses contention but not portability or linearity *)
+let foo (t : ('a -> 'a) option @@ contended) =
+  use_uncontended t
+[%%expect{|
+val foo : ('a : any). ('a -> 'a) option @ contended -> unit = <fun>
+|}]
+
+let foo (t : ('a -> 'a) option @@ nonportable) =
+  use_portable t
+[%%expect{|
+Line 2, characters 15-16:
+2 |   use_portable t
+                   ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : ('a -> 'a) option @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : ('a -> 'a) option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : ('a -> 'a) option @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* references crosses portability but not contention *)
+let foo (t : int ref option @@ contended) =
+    use_uncontended t
+[%%expect{|
+Line 2, characters 20-21:
+2 |     use_uncontended t
+                        ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : int ref option @@ nonportable once) =
+    use_portable t;
+    use_many t
+[%%expect{|
+val foo : int ref option @ once -> unit = <fun>
+|}]
+
+let foo (t : int ref option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : int ref option @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* shouldn't cross anything *)
+let foo (t : ('a -> 'a) ref option @@ contended) =
+  use_uncontended t
+
+[%%expect{|
+Line 2, characters 18-19:
+2 |   use_uncontended t
+                      ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : ('a -> 'a) ref option @@ nonportable) =
+  use_portable t
+
+[%%expect{|
+Line 2, characters 15-16:
+2 |   use_portable t
+                   ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : ('a -> 'a) ref option @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : ('a -> 'a) ref option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : ('a -> 'a) ref option @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* crosses nothing *)
+let foo (t : 'a option @@ contended) =
+    use_uncontended t
+[%%expect{|
+Line 2, characters 20-21:
+2 |     use_uncontended t
+                        ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : 'a option @@ nonportable) =
+    use_portable t
+[%%expect{|
+Line 2, characters 17-18:
+2 |     use_portable t
+                     ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : 'a option @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : 'a option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : 'a option @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* looks at kinds *)
+let foo (type a : value mod uncontended portable)
+      (t : a option @@ contended nonportable) =
+  use_uncontended t;
+  use_portable t
+
+[%%expect{|
+val foo :
+  ('a : value mod uncontended portable). 'a option @ contended -> unit =
+  <fun>
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a option @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a option @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a option @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(**********************************************)
+(* TEST 2: Mode crossing looks through [list] *)
+
+let foo (t : int list @@ contended nonportable once) =
+    use_uncontended t;
+    use_portable t;
+    use_many t
+[%%expect{|
+val foo : int list @ once contended -> unit = <fun>
+|}]
+
+let foo (t : int list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : int list @@ aliased) =
+  use_unique t;
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t;
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* crosses contention but not portability or linearity *)
+let foo (t : ('a -> 'a) list @@ contended) =
+  use_uncontended t
+[%%expect{|
+val foo : ('a : any). ('a -> 'a) list @ contended -> unit = <fun>
+|}]
+
+let foo (t : ('a -> 'a) list @@ nonportable) =
+  use_portable t
+[%%expect{|
+Line 2, characters 15-16:
+2 |   use_portable t
+                   ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : ('a -> 'a) list @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : ('a -> 'a) list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : ('a -> 'a) list @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* references crosses portability but not contention *)
+let foo (t : int ref list @@ contended) =
+    use_uncontended t
+[%%expect{|
+Line 2, characters 20-21:
+2 |     use_uncontended t
+                        ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : int ref list @@ nonportable once) =
+    use_portable t;
+    use_many t
+[%%expect{|
+val foo : int ref list @ once -> unit = <fun>
+|}]
+
+let foo (t : int ref list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : int ref list @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* shouldn't cross anything *)
+let foo (t : ('a -> 'a) ref list @@ contended) =
+  use_uncontended t
+
+[%%expect{|
+Line 2, characters 18-19:
+2 |   use_uncontended t
+                      ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : ('a -> 'a) ref list @@ nonportable) =
+  use_portable t
+
+[%%expect{|
+Line 2, characters 15-16:
+2 |   use_portable t
+                   ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : ('a -> 'a) ref list @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : ('a -> 'a) ref list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : ('a -> 'a) ref list @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* crosses nothing *)
+let foo (t : 'a list @@ contended) =
+    use_uncontended t
+[%%expect{|
+Line 2, characters 20-21:
+2 |     use_uncontended t
+                        ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+let foo (t : 'a list @@ nonportable) =
+    use_portable t
+[%%expect{|
+Line 2, characters 17-18:
+2 |     use_portable t
+                     ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (t : 'a list @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (t : 'a list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (t : 'a list @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(* looks at kinds *)
+let foo (type a : value mod uncontended portable)
+      (t : a list @@ contended nonportable) =
+  use_uncontended t;
+  use_portable t
+
+[%%expect{|
+val foo : ('a : value mod uncontended portable). 'a list @ contended -> unit =
+  <fun>
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a list @@ once) =
+  use_many t
+
+[%%expect{|
+Line 2, characters 11-12:
+2 |   use_many t
+               ^
+Error: This value is "once" but expected to be "many".
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a list @@ local) =
+  use_global t [@nontail]
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_global t [@nontail]
+                 ^
+Error: This value escapes its region.
+|}]
+
+let foo (type a : value mod uncontended portable) (t : a list @@ aliased) =
+  use_unique t
+
+[%%expect{|
+Line 2, characters 13-14:
+2 |   use_unique t
+                 ^
+Error: This value is "aliased" but expected to be "unique".
+|}]
+
+(******************************)
+(* TEST 3: User-written types *)
+
+(* user syntax *)
+type 'a t1 : immutable_data with 'a = { x : 'a }
+
+(* CR layouts v2.8: This should be accepted *)
+(* CR reisenberg: fix! *)
+[%%expect{|
+Line 1, characters 0-48:
+1 | type 'a t1 : immutable_data with 'a = { x : 'a }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "t1" is immutable_data
+         because it's a boxed record type.
+       But the kind of type "t1" must be a subkind of immutable_data
+         because of the annotation on the declaration of the type t1.
+|}]
+
+type 'a t2 : immutable_data with 'a = Foo of 'a
+
+(* CR layouts v2.8: This should be accepted *)
+[%%expect{|
+Line 1, characters 0-47:
+1 | type 'a t2 : immutable_data with 'a = Foo of 'a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The kind of type "t2" is immutable_data
+         because it's a boxed variant type.
+       But the kind of type "t2" must be a subkind of immutable_data
+         because of the annotation on the declaration of the type t2.
+|}]
+
+(*****************)
+(* TEST 4: Loops *)
+
+(* This requires fuel-per-type-head in [Jkind.Bound.reduce_baggage] to cut off
+   *)
+type 'a t = Leaf of 'a | Node of ('a * 'a) t
+
+let rec depth : 'a. 'a t -> _ = function
+  | Leaf _ -> 1
+  | Node x -> 1 + depth x
+
+[%%expect{|
+type 'a t = Leaf of 'a | Node of ('a * 'a) t
+val depth : 'a t -> int = <fun>
+|}]
diff --git a/testsuite/tests/typing-modal-kinds/basics.ml b/testsuite/tests/typing-modal-kinds/basics.ml
index ba08bca752f..7efe33478e6 100644
--- a/testsuite/tests/typing-modal-kinds/basics.ml
+++ b/testsuite/tests/typing-modal-kinds/basics.ml
@@ -279,22 +279,14 @@ val int_duplicate : int = 5
 
 let string_list_duplicate = let once_ x : string list = ["hi";"bye"] in Fun.id x
 
-(* CR layouts v2.8: this should succeed *)
 [%%expect{|
-Line 1, characters 79-80:
-1 | let string_list_duplicate = let once_ x : string list = ["hi";"bye"] in Fun.id x
-                                                                                   ^
-Error: This value is "once" but expected to be "many".
+val string_list_duplicate : string list = ["hi"; "bye"]
 |}]
 
 let int_list_duplicate = let once_ x : int list = [4;5] in Fun.id x
 
-(* CR layouts v2.8: this should succeed *)
 [%%expect{|
-Line 1, characters 66-67:
-1 | let int_list_duplicate = let once_ x : int list = [4;5] in Fun.id x
-                                                                      ^
-Error: This value is "once" but expected to be "many".
+val int_list_duplicate : int list = [4; 5]
 |}]
 
 let hidden_string_duplicate =
@@ -331,12 +323,8 @@ let hidden_int_list_duplicate =
     [Hidden_int.hide 2; Hidden_int.hide 3]
   in Fun.id x
 
-(* CR layouts v2.8: this should succeed *)
 [%%expect{|
-Line 4, characters 12-13:
-4 |   in Fun.id x
-                ^
-Error: This value is "once" but expected to be "many".
+val hidden_int_list_duplicate : Hidden_int.t list = [<abstr>; <abstr>]
 |}]
 
 let float_duplicate = let once_ x : float = 3.14 in Fun.id x
@@ -374,23 +362,15 @@ val hidden_int64_u_duplicate : unit -> Hidden_int64_u.t = <fun>
 let float_u_record_duplicate =
   let once_ x : float_u_record = { x = #3.14; y = #2.718 } in Fun.id x
 
-(* CR layouts v2.8: this should succeed *)
 [%%expect{|
-Line 2, characters 69-70:
-2 |   let once_ x : float_u_record = { x = #3.14; y = #2.718 } in Fun.id x
-                                                                         ^
-Error: This value is "once" but expected to be "many".
+val float_u_record_duplicate : float_u_record = {x = <abstr>; y = <abstr>}
 |}]
 
 let float_u_record_list_duplicate =
   let once_ x : float_u_record list = [] in Fun.id x
 
-(* CR layouts v2.8: this should succeed *)
 [%%expect{|
-Line 2, characters 51-52:
-2 |   let once_ x : float_u_record list = [] in Fun.id x
-                                                       ^
-Error: This value is "once" but expected to be "many".
+val float_u_record_list_duplicate : float_u_record list = []
 |}]
 
 let function_duplicate = let once_ x : int -> int = fun y -> y in Fun.id x
@@ -707,7 +687,7 @@ let ref_immutable_data_right x =
 Line 2, characters 30-53:
 2 |   take_strong_immutable_data (weaken_immutable_data x : float ref);
                                   ^^^^^^^^^^^^^^^^^^^^^^^
-Error: This value is "once" but expected to be "many".
+Error: This value is "contended" but expected to be "uncontended".
 |}]
 
 let ref_immutable_data_left x =
@@ -717,7 +697,7 @@ let ref_immutable_data_left x =
 Line 3, characters 29-30:
 3 |   take_strong_immutable_data x
                                  ^
-Error: This value is "once" but expected to be "many".
+Error: This value is "contended" but expected to be "uncontended".
 |}]
 
 let float_immutable_data_right x =
diff --git a/testsuite/tests/typing-modal-kinds/expected_mode.ml b/testsuite/tests/typing-modal-kinds/expected_mode.ml
index 79a6766e9d5..35ba2f7551f 100644
--- a/testsuite/tests/typing-modal-kinds/expected_mode.ml
+++ b/testsuite/tests/typing-modal-kinds/expected_mode.ml
@@ -221,10 +221,7 @@ Error: This value is "once" but expected to be "many".
 let int_list_duplicate : once_ _ -> int list = fun x -> x
 
 [%%expect{|
-Line 1, characters 56-57:
-1 | let int_list_duplicate : once_ _ -> int list = fun x -> x
-                                                            ^
-Error: This value is "once" but expected to be "many".
+val int_list_duplicate : int list @ once -> int list = <fun>
 |}]
 
 let hidden_string_duplicate : once_ _ -> Hidden_string.t =
@@ -267,10 +264,8 @@ let float_u_record_duplicate : once_ _ -> float_u_record =
   fun x -> x
 
 [%%expect{|
-Line 2, characters 11-12:
-2 |   fun x -> x
-               ^
-Error: This value is "once" but expected to be "many".
+val float_u_record_duplicate : float_u_record @ once -> float_u_record =
+  <fun>
 |}]
 
 let float_u_record_list_duplicate :
@@ -278,10 +273,8 @@ let float_u_record_list_duplicate :
   fun x -> x
 
 [%%expect{|
-Line 3, characters 11-12:
-3 |   fun x -> x
-               ^
-Error: This value is "once" but expected to be "many".
+val float_u_record_list_duplicate :
+  float_u_record list @ once -> float_u_record list = <fun>
 |}]
 
 let function_duplicate : once_ _ -> (int -> int) = fun x -> x
diff --git a/testsuite/tests/typing-unique/unique_documentation.ml b/testsuite/tests/typing-unique/unique_documentation.ml
index df657c53b19..a0a58e96e28 100644
--- a/testsuite/tests/typing-unique/unique_documentation.ml
+++ b/testsuite/tests/typing-unique/unique_documentation.ml
@@ -73,15 +73,10 @@ val get_id : delayed_free @ once -> int = <fun>
 
 type delayed_free = { ids : int list; callback : unit -> unit }
 
-(* This does not work yet, but we expect it to work soon.
-   If you make it work, please update the uniqueness documentation. *)
 let get_ids : delayed_free @ once -> int list @ many = fun d -> d.ids
 [%%expect{|
 type delayed_free = { ids : int list; callback : unit -> unit; }
-Line 5, characters 64-69:
-5 | let get_ids : delayed_free @ once -> int list @ many = fun d -> d.ids
-                                                                    ^^^^^
-Error: This value is "once" but expected to be "many".
+val get_ids : delayed_free @ once -> int list = <fun>
 |}]
 
 let okay t =
diff --git a/tools/debug_printers.ml b/tools/debug_printers.ml
index 259c0c95fd1..a4e430cdbc8 100644
--- a/tools/debug_printers.ml
+++ b/tools/debug_printers.ml
@@ -5,7 +5,7 @@ let path = Path.print
 let ctype_global_state = Ctype.print_global_state
 let sort = Jkind.Sort.Debug_printers.t
 let sort_var = Jkind.Sort.Debug_printers.var
-let jkind = Jkind.Debug_printers.t
+let jkind ppf k = Jkind.Debug_printers.t ~print_type_expr:type_expr ppf k
 let zero_alloc_var = Zero_alloc.debug_printer
 let maybe_unique = Uniqueness_analysis.Maybe_unique.print
 let maybe_aliased = Uniqueness_analysis.Maybe_aliased.print
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 5ec54f99f29..5e43a14ec2c 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1466,6 +1466,13 @@ let instance_parameterized_type ?keep_names sch_args sch =
     (ty_args, ty)
   )
 
+let instance_parameterized_kind args jkind =
+  For_copy.with_scope (fun copy_scope ->
+    let ty_args = List.map (fun t -> copy copy_scope t) args in
+    let jkind = Jkind.map_type_expr (copy copy_scope) jkind in
+    (ty_args, jkind)
+  )
+
 (* [map_kind f kind] maps [f] over all the types in [kind]. [f] must preserve jkinds *)
 let map_kind f = function
   | (Type_abstract _ | Type_open) as k -> k
@@ -1498,6 +1505,7 @@ let instance_declaration decl =
     {decl with type_params = List.map copy decl.type_params;
      type_manifest = Option.map copy decl.type_manifest;
      type_kind = map_kind copy decl.type_kind;
+     type_jkind = Jkind.map_type_expr copy decl.type_jkind;
     }
   )
 
@@ -1828,6 +1836,20 @@ let subst env level priv abbrev oty params args body =
     undo_abbrev ();
     raise Cannot_subst
 
+let jkind_subst env level params args jkind =
+  if List.length params <> List.length args then raise Cannot_subst;
+  let old_level = !current_level in
+  current_level := level;
+  let (params', jkind') = instance_parameterized_kind params jkind in
+  let uenv = Expression {env; in_subst = true} in
+  try
+    List.iter2 (!unify_var' uenv) params' args;
+    current_level := old_level;
+    jkind'
+  with Unify _ ->
+    current_level := old_level;
+    raise Cannot_subst
+
 (* CR layouts: Can we actually just always ignore jkinds in apply/subst?
 
    It seems like almost, but there may be cases where it would forget
@@ -2076,6 +2098,8 @@ let try_expand_safe_opt env ty =
 let expand_head_opt env ty =
   try try_expand_head try_expand_safe_opt env ty with Cannot_expand -> ty
 
+let is_principal ty =
+  not !Clflags.principal || get_level ty = generic_level
 
 type unbox_result =
   (* unboxing process made a step: either an unboxing or removal of a [Tpoly] *)
@@ -2162,11 +2186,23 @@ let rec estimate_type_jkind ~expand_component env ty =
        (List.map (fun (_, ty) ->
           estimate_type_jkind ~expand_component env (expand_component ty)) ltys)
        ~why:Unboxed_tuple
-  | Tconstr (p, _, _) -> begin
-      try
-        (Env.find_type p env).type_jkind
-      with
-        Not_found -> Jkind.Builtin.any ~why:(Missing_cmi p)
+  | Tconstr (p, args, _) -> begin try
+      let type_decl = Env.find_type p env in
+      let jkind = type_decl.type_jkind in
+      (* Checking [has_baggage] here is needed for correctness, because
+         intersection types sometimes do not unify with themselves. Removing
+         this check causes typing-misc/pr7937.ml to fail. *)
+      if Jkind.has_baggage jkind
+      then
+        let level = get_level ty in
+        (* CR layouts v2.8: We could possibly skip this substitution if we're
+           called from [constrain_type_jkind]; the jkind returned without
+           substing is just weaker than the one we would get by substing. *)
+        jkind_subst env level type_decl.type_params args jkind
+      else
+        jkind
+    with
+    | Cannot_subst | Not_found -> Jkind.Builtin.any ~why:(Missing_cmi p)
     end
   | Tobject _ -> Jkind.for_object
   | Tfield _ -> Jkind.Builtin.value ~why:Tfield
@@ -2254,6 +2290,8 @@ let type_jkind env ty =
   let _, jkind = type_jkind_deep env ty ty 100 in
   jkind
 
+(* CR layouts v2.8: This function is quite suspect. See Jane Street internal
+   gdoc titled "Let's kill type_jkind_purely". *)
 let type_jkind_purely env ty =
   if !Clflags.principal || Env.has_local_constraints env then
     (* We snapshot to keep this pure; see the test in [typing-local/crossing.ml]
@@ -2265,14 +2303,26 @@ let type_jkind_purely env ty =
   else
     type_jkind env ty
 
+(* CR layouts v2.8: It's possible we can remove this function if we change
+   [jkind_subst] to not substitute non-principal things. Investigate. *)
+let type_jkind_purely_if_principal env ty =
+  match is_principal ty with
+  | true -> Some (type_jkind_purely env ty)
+  | false -> None
+
 let estimate_type_jkind = estimate_type_jkind ~expand_component:Fun.id
 
 (**** checking jkind relationships ****)
 
+(* forward declaration *)
+let type_equal' = ref (fun _ _ _ -> Misc.fatal_error "type_equal")
+
 (* The ~fixed argument controls what effects this may have on `ty`.  If false,
    then we will update the jkind of type variables to make the check true, if
    possible.  If true, we won't (but will still instantiate sort variables). *)
 let constrain_type_jkind ~fixed env ty jkind =
+  let type_equal = !type_equal' env in
+  let jkind_of_type = type_jkind_purely_if_principal env in
   (* The [expanded] argument says whether we've already tried [expand_head_opt].
 
      The "fuel" argument is used because we're duplicating the loop of
@@ -2321,7 +2371,7 @@ let constrain_type_jkind ~fixed env ty jkind =
           it first.
         *)
        let jkind_inter =
-         Jkind.intersection_or_error
+         Jkind.intersection_or_error ~type_equal ~jkind_of_type
            ~reason:Tyvar_refinement_intersection ty's_jkind jkind
        in
        Result.map (set_var_jkind ty) jkind_inter
@@ -2331,7 +2381,9 @@ let constrain_type_jkind ~fixed env ty jkind =
     | Tpoly (t, _) -> loop ~fuel ~expanded:false t ty's_jkind jkind
 
     | _ ->
-       match Jkind.sub_or_intersect ty's_jkind jkind with
+       match
+         Jkind.sub_or_intersect ~type_equal ~jkind_of_type ty's_jkind jkind
+       with
        | Sub -> Ok ()
        | Disjoint ->
           (* Reporting that [ty's_jkind] must be a subjkind of [jkind] is not
@@ -2423,26 +2475,6 @@ let check_type_externality env ty ext =
   | Ok () -> true
   | Error _ -> false
 
-let check_decl_jkind env decl jkind =
-  (* CR layouts v2.8: This will need to be deeply reimplemented. *)
-  let jkind = Jkind.terrible_relax_l jkind in
-  match Jkind.sub_or_error decl.type_jkind jkind with
-  | Ok () as ok -> ok
-  | Error _ as err ->
-      match decl.type_manifest with
-      | None -> err
-      | Some ty -> check_type_jkind env ty jkind
-
-let constrain_decl_jkind env decl jkind =
-  (* CR layouts v2.8: This will need to be deeply reimplemented. *)
-  let jkind = Jkind.terrible_relax_l jkind in
-  match Jkind.sub_or_error decl.type_jkind jkind with
-  | Ok () as ok -> ok
-  | Error _ as err ->
-      match decl.type_manifest with
-      | None -> err
-      | Some ty -> constrain_type_jkind env ty jkind
-
 let check_type_jkind_exn env texn ty jkind =
   match check_type_jkind env ty jkind with
   | Ok _ -> ()
@@ -2475,25 +2507,39 @@ let rec intersect_type_jkind ~reason env ty1 jkind2 =
   | _ ->
     (* [intersect_type_jkind] is called rarely, so we don't bother with trying
        to avoid this call as in [constrain_type_jkind] *)
-    let ty1 = get_unboxed_type_approximation env ty1 in
-    Jkind.intersect_l_l ~reason (estimate_type_jkind env ty1) jkind2
+    let type_equal = !type_equal' env in
+    let jkind1 = type_jkind env ty1 in
+    let jkind_of_type = type_jkind_purely_if_principal env in
+    let jkind1 = Jkind.round_up ~type_equal ~jkind_of_type jkind1 in
+    let jkind2 = Jkind.round_up ~type_equal ~jkind_of_type jkind2 in
+    Jkind.intersection_or_error ~type_equal ~jkind_of_type ~reason jkind1 jkind2
 
 (* See comment on [jkind_unification_mode] *)
-let unification_jkind_check env ty jkind =
-  match !lmode with
-  | Perform_checks -> constrain_type_jkind_exn env Unify ty jkind
-  | Delay_checks r -> r := (ty,jkind) :: !r
-
-let check_and_update_generalized_ty_jkind ?name ~loc ty =
+let unification_jkind_check uenv ty jkind =
+  (* If we assume the original type is well-kinded, then we don't need to check
+     jkinds in substitution. And checking here can actually cause a loop with
+     with-kinds, in test case typing-misc/constraints.ml, because substitution
+     is used in [estimate_type_jkind], used in [constrain_type_jkind]. *)
+  if not (in_subst_mode uenv) then
+    match !lmode with
+    | Perform_checks -> constrain_type_jkind_exn (get_env uenv) Unify ty jkind
+    | Delay_checks r -> r := (ty,jkind) :: !r
+
+let check_and_update_generalized_ty_jkind ?name ~loc env ty =
   let immediacy_check jkind =
     let is_immediate jkind =
       (* Just check externality and layout, because that's what actually matters
          for upstream code. We check both for a known value and something that
          might turn out later to be value. This is the conservative choice. *)
-      Jkind.(Externality.le (get_externality_upper_bound jkind) External64 &&
-             match get_layout jkind with
-               | Some (Base Value) | None -> true
-               | _ -> false)
+      let type_equal = !type_equal' env in
+      let jkind_of_type = type_jkind_purely_if_principal env in
+      let ext =
+        Jkind.get_externality_upper_bound ~type_equal ~jkind_of_type jkind
+      in
+      Jkind.Externality.le ext External64 &&
+      match Jkind.get_layout jkind with
+      | Some (Base Value) | None -> true
+      | _ -> false
     in
     if Language_extension.erasable_extensions_only ()
       && is_immediate jkind && not (Jkind.History.has_warned jkind)
@@ -3100,9 +3146,11 @@ let equivalent_with_nolabels l1 l2 =
   | (Nolabel | Labelled _), (Nolabel | Labelled _) -> true
   | _ -> false)
 
-(* the [tk] means we're comparing a type against a jkind *)
+(* the [tk] means we're comparing a type against a jkind; axes do
+   not matter, so a jkind extracted from a type_declaration does
+   not need to be substed *)
 let has_jkind_intersection_tk env ty jkind =
-  Jkind.has_intersection_l_l (type_jkind env ty) jkind
+  Jkind.has_intersection (type_jkind env ty) jkind
 
 (* [mcomp] tests if two types are "compatible" -- i.e., if they could ever
    unify.  (This is distinct from [eqtype], which checks if two types *are*
@@ -3256,7 +3304,7 @@ and mcomp_type_decl type_pairs env p1 p2 tl1 tl2 =
     let decl = Env.find_type p1 env in
     let decl' = Env.find_type p2 env in
     let check_jkinds () =
-      if not (Jkind.has_intersection_l_l decl.type_jkind decl'.type_jkind)
+      if not (Jkind.has_intersection decl.type_jkind decl'.type_jkind)
       then raise Incompatible
     in
     if compatible_paths p1 p2 then begin
@@ -3392,11 +3440,13 @@ let add_jkind_equation ~reason uenv destination jkind1 =
         begin
           try
             let decl = Env.find_type p env in
-            if not (Jkind.equal (Jkind.terrible_relax_l jkind)
-                                (Jkind.terrible_relax_l decl.type_jkind))
-            then
-              let refined_decl = { decl with type_jkind = jkind } in
-              set_env uenv (Env.add_local_constraint p refined_decl env);
+            (* CR layouts v2.8: We might be able to do better here. *)
+            match Jkind.try_allow_r jkind, Jkind.try_allow_r decl.type_jkind with
+            | Some jkind, Some decl_jkind when
+                   not (Jkind.equal jkind decl_jkind) ->
+               let refined_decl = { decl with type_jkind = Jkind.disallow_right jkind } in
+               set_env uenv (Env.add_local_constraint p refined_decl env)
+            | _ -> ()
           with
             Not_found -> ()
         end
@@ -3424,6 +3474,11 @@ let add_gadt_equation uenv source destination =
        When we check the jkind later, we may not be able to see the local
        equation because of its scope. *)
     let jkind = jkind_of_abstract_type_declaration env source in
+    let jkind = match Jkind.try_allow_r jkind with
+      | None -> Misc.fatal_errorf "Abstract kind with [with]: %a"
+                  Jkind.format jkind
+      | Some jkind -> jkind
+    in
     add_jkind_equation ~reason:(Gadt_equation source)
       uenv destination jkind;
     (* Adding a jkind equation may change the uenv. *)
@@ -3432,7 +3487,7 @@ let add_gadt_equation uenv source destination =
       new_local_type
         ~manifest_and_scope:(destination, expansion_scope)
         type_origin
-        (Jkind.terrible_relax_l jkind)
+        jkind
     in
     set_env uenv (Env.add_local_constraint source decl env);
     cleanup_abbrev ()
@@ -3537,7 +3592,7 @@ let unify1_var uenv t1 t2 =
   let env = get_env uenv in
   match
     occur_univar_for Unify env t2;
-    unification_jkind_check env t2 (Jkind.disallow_left jkind)
+    unification_jkind_check uenv t2 (Jkind.disallow_left jkind)
   with
   | () ->
       begin
@@ -3565,7 +3620,7 @@ let unify3_var uenv jkind1 t1' t2 t2' =
   let snap = snapshot () in
   match
     occur_univar_for Unify (get_env uenv) t2;
-    unification_jkind_check (get_env uenv) t2' (Jkind.disallow_left jkind1)
+    unification_jkind_check uenv t2' (Jkind.disallow_left jkind1)
   with
   | () -> link_type t1' t2
   | exception Unify_trace _ when in_pattern_mode uenv ->
@@ -4215,11 +4270,7 @@ let unify_var uenv t1 t2 =
         occur_for Unify uenv t1 t2;
         update_level_for Unify env (get_level t1) t2;
         update_scope_for Unify (get_scope t1) t2;
-        (* If we assume the original type is well-kinded, then we don't
-           need to check jkinds in substitution. *)
-        if not (in_subst_mode uenv) then begin
-          unification_jkind_check env t2 (Jkind.disallow_left jkind)
-        end;
+        unification_jkind_check uenv t2 (Jkind.disallow_left jkind);
         link_type t1 t2;
         reset_trace_gadt_instances reset_tracing;
       with Unify_trace trace ->
@@ -4815,8 +4866,10 @@ let relevant_pairs pairs v =
 let mode_cross_left_alloc env ty mode =
   let mode =
     if not (is_principal ty) then mode else
+    let type_equal = !type_equal' env in
     let jkind = type_jkind_purely env ty in
-    let upper_bounds = Jkind.get_modal_upper_bounds jkind in
+    let jkind_of_type = type_jkind_purely_if_principal env in
+    let upper_bounds = Jkind.get_modal_upper_bounds ~type_equal ~jkind_of_type jkind in
     Alloc.meet_const upper_bounds mode
   in
   mode |> Alloc.disallow_right
@@ -4825,8 +4878,12 @@ let mode_cross_left_alloc env ty mode =
    are likely bugs there, too. *)
 let mode_cross_right env ty mode =
   if not (is_principal ty) then Alloc.disallow_left mode else
+  let type_equal = !type_equal' env in
   let jkind = type_jkind_purely env ty in
-  let upper_bounds = Jkind.get_modal_upper_bounds jkind in
+  let jkind_of_type = type_jkind_purely_if_principal env in
+  let upper_bounds =
+    Jkind.get_modal_upper_bounds ~type_equal ~jkind_of_type jkind
+  in
   Alloc.imply upper_bounds mode
 
 let submode_with_cross env ~is_ret ty l r =
@@ -6769,6 +6826,14 @@ let nondep_type_decl env mid is_covariant decl =
                 Private
             with Nondep_cannot_erase _ ->
               None, decl.type_private
+    and jkind =
+      try Jkind.map_type_expr (nondep_type_rec env mid) decl.type_jkind
+      (* CR layouts v2.8: I have no idea what I'm doing on this next line. *)
+      with Nondep_cannot_erase _ when is_covariant ->
+        let type_equal = !type_equal' env in
+        let jkind_of_type = type_jkind_purely_if_principal env in
+        Jkind.round_up ~type_equal ~jkind_of_type decl.type_jkind |>
+        Jkind.disallow_right
     in
     clear_hash ();
     let priv =
@@ -6779,7 +6844,7 @@ let nondep_type_decl env mid is_covariant decl =
     { type_params = params;
       type_arity = decl.type_arity;
       type_kind = tk;
-      type_jkind = decl.type_jkind;
+      type_jkind = jkind;
       type_manifest = tm;
       type_private = priv;
       type_variance = decl.type_variance;
@@ -6948,3 +7013,54 @@ let print_global_state fmt global_state =
     print_field fmt "global_level" global_level;
   in
   Format.fprintf fmt "@[<1>{@;%a}@]" print_fields global_state
+
+              (*******************************)
+              (* checking declaration jkinds *)
+              (* this is down here so it can use [is_equal] *)
+
+(* CR layouts v2.8: Passing this function everywhere is annoying. Instead,
+   it would be good just to use mutation to make this accessible in jkind.ml.
+   The problem is that Env depends on Jkind, and so the type of [type_equal]
+   can't be written in Jkind. It's possible that, after jkind.ml is broken up,
+   this problem goes away, because the dependency from Env to Jkind is pretty
+   minimal. *)
+let type_equal env ty1 ty2 = is_equal env false [ty1] [ty2]
+let () = type_equal' := type_equal
+
+let check_decl_jkind env decl jkind =
+  (* CR layouts v2.8: This could use an algorithm like [constrain_type_jkind]
+     to expand only as much as needed, but the l/l subtype algorithm is tricky,
+     and so we leave this optimization for later. *)
+  let type_equal = type_equal env in
+  let jkind_of_type ty = Some (type_jkind_purely env ty) in
+  match Jkind.sub_jkind_l ~type_equal ~jkind_of_type decl.type_jkind jkind with
+  | Ok _ -> Ok ()
+  | Error _ as err ->
+    match decl.type_manifest with
+    | None -> err
+    | Some ty ->
+      (* CR layouts v2.8: Should this use [type_jkind_purely_if_principal]? I
+         think not. *)
+      let ty_jkind = type_jkind env ty in
+      match Jkind.sub_jkind_l ~type_equal ~jkind_of_type ty_jkind jkind with
+      | Ok _ -> Ok ()
+      | Error _ as err -> err
+
+let constrain_decl_jkind env decl jkind =
+  (* CR layouts v2.8: This will need to be deeply reimplemented. *)
+  match Jkind.try_allow_r jkind with
+  (* This case is sad, because it can't refine type variables. Hence
+     the need for reimplementation. Hopefully no one hits this for
+     a while. *)
+  | None -> check_decl_jkind env decl jkind
+  | Some jkind ->
+    let type_equal = type_equal env in
+    let jkind_of_type ty = Some (type_jkind_purely env ty) in
+    match
+      Jkind.sub_or_error ~type_equal ~jkind_of_type decl.type_jkind jkind
+    with
+    | Ok () as ok -> ok
+    | Error _ as err ->
+        match decl.type_manifest with
+        | None -> err
+        | Some ty -> constrain_type_jkind env ty jkind
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 6caadd85790..8fa4e6b65ea 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -598,6 +598,11 @@ val type_jkind : Env.t -> type_expr -> jkind_l
    expansion. *)
 val type_jkind_purely : Env.t -> type_expr -> jkind_l
 
+(* Like [type_jkind_purely], but returns [None] if the type is not
+   principally known. Useful to instantiate [jkind_of_type] in various
+   functions exported by [Jkind]. *)
+val type_jkind_purely_if_principal : Env.t -> type_expr -> jkind_l option
+
 (* Find a type's sort (if fixed is false: constraining it to be an
    arbitrary sort variable, if needed) *)
 val type_sort :
@@ -624,6 +629,10 @@ val check_decl_jkind :
 val constrain_decl_jkind :
   Env.t -> type_declaration -> jkind_l -> (unit, Jkind.Violation.t) result
 
+(* Compare two types for equality, with no renaming. This is useful for
+   the [type_equal] function that must be passed to certain jkind functions. *)
+val type_equal: Env.t -> type_expr -> type_expr -> bool
+
 val check_type_jkind :
   Env.t -> type_expr -> ('l * allowed) jkind -> (unit, Jkind.Violation.t) result
 val constrain_type_jkind :
@@ -678,7 +687,7 @@ val check_type_externality : Env.t -> type_expr -> Jkind.Externality.t -> bool
 
    *)
 val check_and_update_generalized_ty_jkind :
-  ?name:Ident.t -> loc:Location.t -> type_expr -> unit
+  ?name:Ident.t -> loc:Location.t -> Env.t -> type_expr -> unit
 
 (* False if running in principal mode and the type is not principal.
    True otherwise. *)
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index 4d4ccb6ad01..e0abdc6bd12 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -70,10 +70,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep =
       in
       let type_params = TypeSet.elements arg_vars_set in
       let arity = List.length type_params in
-      let is_void_label lbl = Jkind.Sort.Const.(equal void lbl.ld_sort) in
-      let jkind =
-        Jkind.for_boxed_record ~all_void:(List.for_all is_void_label lbls)
-      in
+      let jkind = Jkind.for_boxed_record lbls in
       let tdecl =
         {
           type_params;
diff --git a/typing/includecore.ml b/typing/includecore.ml
index a4d5cd2bb97..6a6677e86cd 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -1323,14 +1323,21 @@ let type_declarations ?(equality = false) ~loc env ~mark name
   in
   let err = match (decl1.type_kind, decl2.type_kind) with
       (_, Type_abstract _) ->
-       (* Note that [decl2.type_jkind] is an upper bound.
-          If it isn't tight, [decl2] must
-          have a manifest, which we're already checking for equality
-          above. Similarly, [decl1]'s kind may conservatively approximate its
-          jkind, but [check_decl_jkind] will expand its manifest.  *)
-        (match Ctype.check_decl_jkind env decl1 decl2.type_jkind with
-         | Ok _ -> None
-         | Error v -> Some (Jkind v))
+        (* No need to check jkinds if decl2 has a manifest; we've already
+           checked for type equality, above. Oddly, this is not just an
+           optimization; unconditionally checking jkinds causes a failure
+           around recursive modules (test case: shapes/recmodules.ml).
+           Richard spent several hours trying to understand what was going
+           on there (after the substitution in [Typemod.check_recmodule_inclusion],
+           there was a type_declaration whose [type_jkind] didn't match its
+           [type_manifest]), but just skipping this check when there is a
+           manifest fixes the problem. *)
+        if Option.is_none decl2.type_manifest then
+          (* Note that [decl2.type_jkind] is an upper bound *)
+          match Ctype.check_decl_jkind env decl1 decl2.type_jkind with
+           | Ok _ -> None
+           | Error v -> Some (Jkind v)
+        else None
     | (Type_variant (cstrs1, rep1), Type_variant (cstrs2, rep2)) ->
         if mark then begin
           let mark usage cstrs =
diff --git a/typing/jkind.ml b/typing/jkind.ml
index fdd5ac0de3c..05212f8d514 100644
--- a/typing/jkind.ml
+++ b/typing/jkind.ml
@@ -14,6 +14,7 @@
 
 open Mode
 open Jkind_types
+open Jkind_axis
 
 [@@@warning "+9"]
 
@@ -290,9 +291,8 @@ module Layout = struct
     pp_element ~nested:false ppf layout
 end
 
-module Externality = Jkind_axis.Externality
-module Nullability = Jkind_axis.Nullability
-module Modes = Jkind_axis.Of_lattice (Alloc.Const)
+module Externality = Externality
+module Nullability = Nullability
 
 module History = struct
   include Jkind_intf.History
@@ -315,8 +315,6 @@ end
 (*********************************)
 (* Main type declarations *)
 
-type +'d const = (type_expr, 'd) Jkind_types.Const.t
-
 type 'd t = (type_expr, 'd) Jkind_types.t
 
 type jkind_l = (allowed * disallowed) t
@@ -326,19 +324,28 @@ type packed = Pack : 'd t -> packed [@@unboxed]
 include Allowance.Magic_allow_disallow (struct
   type (_, _, 'd) sided = 'd t
 
-  let disallow_right ({ jkind = { layout = _; _ }; _ } as t) = t
+  let disallow_right t =
+    { t with jkind = Layout_and_axes.disallow_right t.jkind }
 
-  let disallow_left ({ jkind = { layout = _; _ }; _ } as t) = t
+  let disallow_left t = { t with jkind = Layout_and_axes.disallow_left t.jkind }
 
-  let allow_right ({ jkind = { layout = _; _ }; _ } as t) = t
+  let allow_right t = { t with jkind = Layout_and_axes.allow_right t.jkind }
 
-  let allow_left ({ jkind = { layout = _; _ }; _ } as t) = t
+  let allow_left t = { t with jkind = Layout_and_axes.allow_left t.jkind }
 end)
 
-let terrible_relax_l ({ jkind = { layout = _; _ }; _ } as t) = t
+let try_allow_r t =
+  Option.map
+    (fun jkind -> { t with jkind })
+    (Layout_and_axes.try_allow_r t.jkind)
 
 let fresh_jkind jkind ~annotation ~why =
   { jkind; annotation; history = Creation why; has_warned = false }
+  |> allow_left |> allow_right
+
+(* This version propagates the allowances from the [jkind] to the output. *)
+let fresh_jkind_poly jkind ~annotation ~why =
+  { jkind; annotation; history = Creation why; has_warned = false }
 
 (******************************)
 (*** user errors ***)
@@ -355,56 +362,332 @@ module Error = struct
         { from_annotation : Parsetree.jkind_annotation;
           from_attribute : Builtin_attributes.jkind_attribute Location.loc
         }
+    | Modded_bound_with_baggage_constraints : 'a Axis.t -> t
+    | With_on_right
 
   exception User_error of Location.t * t
 end
 
 let raise ~loc err = raise (Error.User_error (loc, err))
 
-module Const = struct
-  open Jkind_types.Layout_and_axes
-
-  type +'d t = 'd const
+(******************************)
+(*** Bounds, specialized to the real [type_expr] ***)
+
+module Baggage = struct
+  include Jkind_types.Baggage
+
+  type nonrec 'd t = (type_expr, 'd) t
+
+  (* You might think that we can only do joins on the left. But that's not true!
+     We can join constants. The important thing is that the allowances of both
+     arguments are the same and that they match the result: this will mean that
+     if we have any baggage in either argument, the result is an l-Baggage, as
+     required. This might change once we have arrow kinds, but we'll deal with
+     that when we get there. *)
+  let join (type l r) (bag1 : (l * r) t) (bag2 : (l * r) t) : (l * r) t =
+    match bag1, bag2 with
+    | No_baggage, No_baggage -> No_baggage
+    | No_baggage, b -> b
+    | b, No_baggage -> b (* CR layouts v2.8: List concatentation is slow. *)
+    | Baggage (ty1, tys1), Baggage (ty2, tys2) ->
+      Baggage (ty1, tys1 @ (ty2 :: tys2))
+
+  let meet (type l1 l2) (bag1 : (l1 * allowed) t) (bag2 : (l2 * allowed) t) :
+      (l1 * allowed) t =
+    match bag1, bag2 with No_baggage, No_baggage -> No_baggage
+
+  let add_baggage (t : (allowed * 'r) t) baggage : (allowed * 'r) t =
+    match t with
+    | No_baggage -> Baggage (baggage, [])
+    | Baggage (ty, tys) -> Baggage (baggage, ty :: tys)
+end
 
-  include Allowance.Magic_allow_disallow (struct
-    type (_, _, 'd) sided = 'd t
+module Bound = struct
+  include Jkind_types.Bound
+
+  type nonrec ('d, 'a) t = (type_expr, 'd, 'a) t
+
+  let simple modifier = { modifier; baggage = No_baggage }
+
+  let join (type axis) ~(axis : axis Axis.t) { modifier = mod1; baggage = bag1 }
+      { modifier = mod2; baggage = bag2 } =
+    let (module Ops) = Axis.get axis in
+    { modifier = Ops.join mod1 mod2; baggage = Baggage.join bag1 bag2 }
+
+  let meet (type axis) ~(axis : axis Axis.t) { modifier = mod1; baggage = bag1 }
+      { modifier = mod2; baggage = bag2 } =
+    let (module Ops) = Axis.get axis in
+    { modifier = Ops.meet mod1 mod2; baggage = Baggage.meet bag1 bag2 }
+
+  let reduce_baggage (type a) ~type_equal ~jkind_of_type ~(axis : a Axis.t)
+      modifier baggage =
+    (* Sadly, it seems hard (impossible?) to be sure to expand all types
+       here without using a fuel parameter to stop infinite regress. Here
+       is a nasty case:
+
+       {[
+         type zero
+         type 'n succ
+
+         type 'n loopy = Mk of 'n succ loopy list [@@unboxed]
+       ]}
+
+       First off: this type *is* inhabited, because of the [list] intervening
+       type (which can be empty). It's also inhabited by various circular
+       structures.
+
+       But what's the jkind of ['n loopy]? It must be the jkind of
+       ['n succ loopy list], which is [immutable_data with 'n succ loopy].
+       In order to see if we shouldn't mode-cross, we have to expand the
+       ['n succ loopy] in the jkind, but expanding that just yields the need
+       to expand ['n succ succ loopy], and around we go.
+
+       It seems hard to avoid this problem. And so we use fuel. Yet we want
+       both a small amount of fuel (a type like [type t = K of (t * t) list]
+       gets big very quickly) and a lot of fuel (we can imagine using a unit
+       of fuel for each level of a deeply nested record structure). The
+       compromise is to track fuel per type head, where a type head is either
+       the path to a type constructor (like [t] or [loopy]) or a tuple.
+       (We need to include tuples because of the possibility of recursive
+       types and the fact that tuples track their element types in their
+       jkind's baggage.)
+
+       The initial fuel per type head is 10, as it seems hard to imagine that
+       we're going to make meaningful progress if we've seen the same type
+       head 10 times in one line of recursive descent. (This "one line of
+       recursive descent" bit is why we recur separately down one type before
+       iterating down the list.)
+    *)
+    (* CR reisenberg: document seen_args *)
+    (* CR layouts v2.8: This would seem to eliminate the possibility of
+       mode-crossing for types like rose trees. There's a good chance
+       normalization will fix this. Once we have normalization, let's try this
+       out. *)
+    let module Loop_control = struct
+      type t =
+        { tuple_fuel : int;
+          constr : (int * type_expr list) Path.Map.t
+        }
 
-    let disallow_left ({ layout = _; _ } as t) = t
+      type result =
+        | Stop (* give up, returning [max] *)
+        | Skip (* skip reducing this type, but otherwise continue *)
+        | Continue of t (* continue, with a new [t] *)
+
+      let initial_fuel_per_ty = 10
+
+      let starting =
+        { tuple_fuel = initial_fuel_per_ty; constr = Path.Map.empty }
+
+      let rec check ({ tuple_fuel; constr } as t) ty =
+        match Types.get_desc ty with
+        | Tpoly (ty, _) -> check t ty
+        | Ttuple _ ->
+          if tuple_fuel > 0
+          then Continue { t with tuple_fuel = tuple_fuel - 1 }
+          else Stop
+        | Tconstr (p, args, _) -> (
+          match Path.Map.find_opt p constr with
+          | None ->
+            Continue
+              { t with
+                constr = Path.Map.add p (initial_fuel_per_ty, args) constr
+              }
+          | Some (fuel, seen_args) ->
+            if List.for_all2 type_equal seen_args args
+            then Skip
+            else if fuel > 0
+            then
+              Continue
+                { t with constr = Path.Map.add p (fuel - 1, args) constr }
+            else Stop)
+        | Tvar _ | Tarrow _ | Tunboxed_tuple _ | Tobject _ | Tfield _ | Tnil
+        | Tvariant _ | Tunivar _ | Tpackage _ ->
+          (* these cases either cannot be infinitely recursive or their jkinds
+             do not have baggage *)
+          Continue t
+        | Tlink _ | Tsubst _ ->
+          Misc.fatal_error "Tlink or Tsubst in reduce_baggage"
+    end in
+    let (module A) = Axis.get axis in
+    let rec loop ctl bound_so_far = function
+      (* early cutoff *)
+      | _ when A.le A.max bound_so_far -> bound_so_far
+      | [] -> bound_so_far
+      | b :: bs -> (
+        match Loop_control.check ctl b with
+        | Stop -> A.max (* out of fuel *)
+        | Skip -> loop ctl bound_so_far bs (* skip [b] *)
+        | Continue ctl_after_unpacking_b -> (
+          match jkind_of_type b with
+          | Some b_jkind ->
+            let b_bound = Bounds.get ~axis b_jkind.jkind.upper_bounds in
+            let bound_so_far = A.join bound_so_far b_bound.modifier in
+            let bound_so_far =
+              loop ctl_after_unpacking_b bound_so_far
+                (Baggage.as_list b_bound.baggage)
+            in
+            (* Use *original* ctl here, so we don't fall over on
+               a record with 20 lists with different payloads. *)
+            loop ctl bound_so_far bs
+          | None ->
+            (* hd is not principally known, so we treat it as having the max
+               bound *)
+            (* CR layouts v2.8: Does this ever trigger? Richard is skeptical
+               that we need to worry about principality here. *)
+            A.max))
+    in
+    loop Loop_control.starting modifier baggage
+
+  let reduce ~type_equal ~jkind_of_type ~axis bound =
+    reduce_baggage ~type_equal ~jkind_of_type ~axis bound.modifier
+      (Baggage.as_list bound.baggage)
+
+  let less_or_equal :
+      type axis l r.
+      type_equal:_ ->
+      jkind_of_type:_ ->
+      axis:axis Axis.t ->
+      (allowed * r, axis) t ->
+      (l * allowed, axis) t ->
+      Misc.Le_result.t =
+   fun ~type_equal ~jkind_of_type ~axis { modifier = m1; baggage = b1 }
+       { modifier = m2; baggage = b2 } ->
+    let (module Axis_ops) = Axis.get axis in
+    match b1, b2 with
+    | No_baggage, No_baggage -> Axis_ops.less_or_equal m1 m2
+    (* CR layouts v2.8: This should expand types on the left. *)
+    | Baggage (ty, tys), No_baggage ->
+      if Axis_ops.le Axis_ops.max m2
+      then Less
+      else
+        let m1' =
+          reduce_baggage ~type_equal ~jkind_of_type ~axis m1 (ty :: tys)
+        in
+        Axis_ops.less_or_equal m1' m2
+end
 
-    let disallow_right ({ layout = _; _ } as t) = t
+module Bounds = struct
+  include Jkind_types.Bounds
 
-    let allow_left ({ layout = _; _ } as t) = t
+  type nonrec 'd t = (type_expr, 'd) t
 
-    let allow_right ({ layout = _; _ } as t) = t
-  end)
+  let min =
+    Create.f
+      { f =
+          (fun (type axis) ~(axis : axis Axis.t) ->
+            let (module Bound_ops) = Axis.get axis in
+            Bound.simple Bound_ops.min)
+      }
 
   let max =
-    { layout = Layout.Const.max;
-      modes_upper_bounds = Modes.max;
-      externality_upper_bound = Externality.max;
-      nullability_upper_bound = Nullability.max
+    Create.f
+      { f =
+          (fun (type axis) ~(axis : axis Axis.t) ->
+            let (module Bound_ops) = Axis.get axis in
+            Bound.simple Bound_ops.max)
+      }
+
+  let simple ~locality ~linearity ~uniqueness ~portability ~contention
+      ~externality ~nullability =
+    { locality = Bound.simple locality;
+      linearity = Bound.simple linearity;
+      uniqueness = Bound.simple uniqueness;
+      portability = Bound.simple portability;
+      contention = Bound.simple contention;
+      externality = Bound.simple externality;
+      nullability = Bound.simple nullability
     }
 
-  let equal_after_all_inference_is_done t1 t2 =
-    Layout_and_axes.equal_after_all_inference_is_done Layout.Const.equal t1 t2
+  let join bounds1 bounds2 = Map2.f { f = Bound.join } bounds1 bounds2
+
+  let meet bounds1 bounds2 = Map2.f { f = Bound.meet } bounds1 bounds2
+
+  let less_or_equal ~type_equal ~jkind_of_type bounds1 bounds2 =
+    Fold2.f
+      { f =
+          (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 ->
+            Bound.less_or_equal ~type_equal ~jkind_of_type ~axis bound1 bound2)
+      }
+      ~combine:Misc.Le_result.combine bounds1 bounds2
+
+  let add_baggage ~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)
+      }
+      bounds
+
+  let has_baggage bounds =
+    Fold.f
+      { f = (fun ~axis:_ bound -> Baggage.has_baggage bound.baggage) }
+      ~combine:( || ) bounds
+end
+
+(***********************)
+(*** constant jkinds ***)
+
+module Context_with_transl = struct
+  type 'd t =
+    | Right_jkind :
+        ('l * allowed) History.annotation_context
+        -> ('l * allowed) t
+    | Left_jkind :
+        (Parsetree.core_type -> Types.type_expr)
+        * (allowed * disallowed) History.annotation_context
+        -> (allowed * disallowed) t
+
+  let get_context : type l r. (l * r) t -> (l * r) History.annotation_context =
+    function
+    | Right_jkind ctx -> ctx
+    | Left_jkind (_, ctx) -> ctx
+end
+
+let print_type_expr =
+  ref (fun ppf _ -> Format.fprintf ppf "ERROR: unset [Jkind.print_type_expr]")
+
+let set_print_type_expr p = print_type_expr := p
+
+module Const = struct
+  open Jkind_types.Layout_and_axes
+
+  type 'd t = (type_expr, 'd) Jkind_types.Const.t
+
+  include Layout_and_axes.Allow_disallow
+
+  let max = { layout = Layout.Const.max; upper_bounds = Bounds.max }
+
+  let no_baggage_and_equal t1 t2 =
+    let open Misc.Stdlib.Monad.Option.Syntax in
+    let t1_t2 =
+      let* t1 = try_allow_l t1 in
+      let* t1 = try_allow_r t1 in
+      let* t2 = try_allow_l t2 in
+      let* t2 = try_allow_r t2 in
+      Some (t1, t2)
+    in
+    match t1_t2 with
+    | Some (t1, t2) -> equal Layout.Const.equal t1 t2
+    | None -> false
 
   module Builtin = struct
-    type nonrec +'d t =
-      { jkind : 'd t;
+    type nonrec t =
+      { jkind : (allowed * allowed) t;
         name : string
       }
 
     let mk_jkind ~mode_crossing ~nullability (layout : Layout.Const.t) =
-      let modes_upper_bounds, externality_upper_bound =
+      let upper_bounds =
         match mode_crossing with
-        | true -> Modes.min, Externality.min
-        | false -> Modes.max, Externality.max
+        | true -> { Bounds.min with nullability = Bound.simple nullability }
+        | false -> { Bounds.max with nullability = Bound.simple nullability }
       in
-      { layout;
-        modes_upper_bounds;
-        externality_upper_bound;
-        nullability_upper_bound = nullability
-      }
+      { layout; upper_bounds }
 
     let any =
       { jkind = mk_jkind Any ~mode_crossing:false ~nullability:Maybe_null;
@@ -430,15 +713,12 @@ module Const = struct
     let immutable_data =
       { jkind =
           { layout = Base Value;
-            modes_upper_bounds =
-              { linearity = Linearity.Const.min;
-                contention = Contention.Const.min;
-                portability = Portability.Const.min;
-                uniqueness = Uniqueness.Const.max;
-                areality = Locality.Const.max
-              };
-            externality_upper_bound = Externality.max;
-            nullability_upper_bound = Nullability.Non_null
+            upper_bounds =
+              Bounds.simple ~linearity:Linearity.Const.min
+                ~contention:Contention.Const.min
+                ~portability:Portability.Const.min
+                ~uniqueness:Uniqueness.Const.max ~locality:Locality.Const.max
+                ~externality:Externality.max ~nullability:Nullability.Non_null
           };
         name = "immutable_data"
       }
@@ -446,15 +726,12 @@ module Const = struct
     let mutable_data =
       { jkind =
           { layout = Base Value;
-            modes_upper_bounds =
-              { linearity = Linearity.Const.min;
-                contention = Contention.Const.max;
-                portability = Portability.Const.min;
-                uniqueness = Uniqueness.Const.max;
-                areality = Locality.Const.max
-              };
-            externality_upper_bound = Externality.max;
-            nullability_upper_bound = Nullability.Non_null
+            upper_bounds =
+              Bounds.simple ~linearity:Linearity.Const.min
+                ~contention:Contention.Const.max
+                ~portability:Portability.Const.min
+                ~uniqueness:Uniqueness.Const.max ~locality:Locality.Const.max
+                ~externality:Externality.max ~nullability:Nullability.Non_null
           };
         name = "mutable_data"
       }
@@ -501,7 +778,13 @@ module Const = struct
        meeting the conditions.
     *)
     let immediate64 =
-      { jkind = { immediate.jkind with externality_upper_bound = External64 };
+      { jkind =
+          { immediate.jkind with
+            upper_bounds =
+              { immediate.jkind.upper_bounds with
+                externality = Bound.simple Externality.External64
+              }
+          };
         name = "immediate64"
       }
 
@@ -560,7 +843,7 @@ module Const = struct
         bits64;
         vec128 ]
 
-    let of_attribute : Builtin_attributes.jkind_attribute -> _ t = function
+    let of_attribute : Builtin_attributes.jkind_attribute -> t = function
       | Immediate -> immediate
       | Immediate64 -> immediate64
   end
@@ -580,43 +863,42 @@ module Const = struct
         modal_bounds : string list
       }
 
-    module Bounds = struct
-      type t =
-        { alloc_bounds : Alloc.Const.t;
-          externality_bound : Externality.t;
-          nullability_bound : Nullability.t
-        }
-
-      let of_jkind jkind =
-        { alloc_bounds = jkind.modes_upper_bounds;
-          externality_bound = jkind.externality_upper_bound;
-          nullability_bound = jkind.nullability_upper_bound
-        }
-    end
-
-    let get_modal_bound ~le ~print ~base actual =
-      match le actual base with
-      | true -> (
-        match le base actual with
-        | true -> `Valid None
-        | false -> `Valid (Some (Format.asprintf "%a" print actual)))
-      | false -> `Invalid
-
-    let get_modal_bounds ~(base : Bounds.t) (actual : Bounds.t) =
-      [ get_modal_bound ~le:Locality.Const.le ~print:Locality.Const.print
-          ~base:base.alloc_bounds.areality actual.alloc_bounds.areality;
-        get_modal_bound ~le:Uniqueness.Const.le ~print:Uniqueness.Const.print
-          ~base:base.alloc_bounds.uniqueness actual.alloc_bounds.uniqueness;
-        get_modal_bound ~le:Linearity.Const.le ~print:Linearity.Const.print
-          ~base:base.alloc_bounds.linearity actual.alloc_bounds.linearity;
-        get_modal_bound ~le:Contention.Const.le ~print:Contention.Const.print
-          ~base:base.alloc_bounds.contention actual.alloc_bounds.contention;
-        get_modal_bound ~le:Portability.Const.le ~print:Portability.Const.print
-          ~base:base.alloc_bounds.portability actual.alloc_bounds.portability;
-        get_modal_bound ~le:Externality.le ~print:Externality.print
-          ~base:base.externality_bound actual.externality_bound;
-        get_modal_bound ~le:Nullability.le ~print:Nullability.print
-          ~base:base.nullability_bound actual.nullability_bound ]
+    let get_baggage : type l r. (l * r) Baggage.t -> _ = function
+      | No_baggage -> ""
+      | Baggage (ty, tys) ->
+        Format.asprintf " with %a"
+          (Format.pp_print_list ~pp_sep:Format.pp_print_space !print_type_expr)
+          (ty :: tys)
+
+    let get_modal_bound (type a) ~(axis : a Axis.t) ~(base : ('d1, a) Bound.t)
+        (actual : ('d2, a) Bound.t) =
+      let (module A) = Axis.get axis in
+      let type_equal _ _ = false in
+      let jkind_of_type _ = None in
+      (* CR layouts v2.8: Fix printing! *)
+      let less_or_equal a b =
+        let open Misc.Stdlib.Monad.Option.Syntax in
+        let* a = Bound.try_allow_l a in
+        let* b = Bound.try_allow_r b in
+        Some (Bound.less_or_equal ~type_equal ~jkind_of_type ~axis a b)
+      in
+      match less_or_equal actual base with
+      | Some Less | Some Equal -> (
+        match less_or_equal base actual with
+        | Some Less | Some Equal -> `Valid None
+        | None | Some Not_le ->
+          `Valid
+            (Some
+               (Format.asprintf "%a%s" A.print actual.modifier
+                  (get_baggage actual.baggage))))
+      | None | Some Not_le -> `Invalid
+
+    let get_modal_bounds ~(base : _ Bounds.t) (actual : _ Bounds.t) =
+      Axis.all
+      |> List.map (fun (Axis.Pack axis) ->
+             let base = Bounds.get ~axis base in
+             let actual = Bounds.get ~axis actual in
+             get_modal_bound ~axis ~base actual)
       |> List.rev
       |> List.fold_left
            (fun acc mode ->
@@ -627,14 +909,12 @@ module Const = struct
            (Some [])
 
     (** Write [actual] in terms of [base] *)
-    let convert_with_base ~(base : _ Builtin.t) actual =
+    let convert_with_base ~(base : Builtin.t) actual =
       let matching_layouts =
         Layout.Const.equal base.jkind.layout actual.layout
       in
       let modal_bounds =
-        get_modal_bounds
-          ~base:(Bounds.of_jkind base.jkind)
-          (Bounds.of_jkind actual)
+        get_modal_bounds ~base:base.jkind.upper_bounds actual.upper_bounds
       in
       match matching_layouts, modal_bounds with
       | true, Some modal_bounds -> Some { base = base.name; modal_bounds }
@@ -653,6 +933,18 @@ module Const = struct
       | [] -> None
 
     let convert jkind =
+      let jkind =
+        if Language_extension.(is_at_least Layouts Alpha)
+        then jkind
+        else
+          { jkind with
+            upper_bounds =
+              Bounds.Map.f
+                { f = (fun ~axis:_ bound -> { bound with baggage = No_baggage })
+                }
+                jkind.upper_bounds
+          }
+      in
       (* For each primitive jkind, we try to print the jkind in terms of it (this is
          possible if the primitive is a subjkind of it). We then choose the "simplest". The
            "simplest" is taken to mean the one with the least number of modes that need to
@@ -675,9 +967,10 @@ module Const = struct
               ~base:
                 { jkind =
                     { layout = jkind.layout;
-                      modes_upper_bounds = Modes.max;
-                      externality_upper_bound = Externality.max;
-                      nullability_upper_bound = Nullability.Non_null
+                      upper_bounds =
+                        { Bounds.max with
+                          nullability = Bound.simple Nullability.Non_null
+                        }
                     };
                   name = Layout.Const.to_string jkind.layout
                 }
@@ -690,12 +983,7 @@ module Const = struct
             let out_jkind_verbose =
               convert_with_base
                 ~base:
-                  { jkind =
-                      { layout = jkind.layout;
-                        modes_upper_bounds = Modes.max;
-                        externality_upper_bound = Externality.max;
-                        nullability_upper_bound = Nullability.max
-                      };
+                  { jkind = { layout = jkind.layout; upper_bounds = Bounds.max };
                     name = Layout.Const.to_string jkind.layout
                   }
                 jkind
@@ -716,34 +1004,23 @@ module Const = struct
 
   let format ppf jkind = to_out_jkind_const jkind |> !Oprint.out_jkind_const ppf
 
+  (*******************************)
+  (* converting user annotations *)
+
   let jkind_of_product_annotations jkinds =
-    let folder (layouts, mode_ub, ext_ub, null_ub)
-        { layout;
-          modes_upper_bounds;
-          externality_upper_bound;
-          nullability_upper_bound
-        } =
-      ( layout :: layouts,
-        Modes.join mode_ub modes_upper_bounds,
-        Externality.join ext_ub externality_upper_bound,
-        Nullability.join null_ub nullability_upper_bound )
+    let folder (layouts_acc, upper_bounds_acc) { layout; upper_bounds } =
+      layout :: layouts_acc, Bounds.join upper_bounds upper_bounds_acc
     in
-    let layouts, mode_ub, ext_ub, null_ub =
+    let layouts, upper_bounds =
       List.fold_left folder
-        ([], Modes.min, Externality.min, Nullability.min)
+        ([], Bounds.min |> Bounds.allow_left |> Bounds.allow_right)
         jkinds
     in
-    { layout = Layout.Const.Product (List.rev layouts);
-      modes_upper_bounds = mode_ub;
-      externality_upper_bound = ext_ub;
-      nullability_upper_bound = null_ub
-    }
+    { layout = Layout.Const.Product (List.rev layouts); upper_bounds }
 
   let rec of_user_written_annotation_unchecked_level :
       type l r.
-      (l * r) History.annotation_context ->
-      Parsetree.jkind_annotation ->
-      (l * r) t =
+      (l * r) Context_with_transl.t -> Parsetree.jkind_annotation -> (l * r) t =
    fun context jkind ->
     match jkind.pjkind_desc with
     | Abbreviation name ->
@@ -762,37 +1039,52 @@ module Const = struct
       | "bits32" -> Builtin.bits32.jkind
       | "bits64" -> Builtin.bits64.jkind
       | "vec128" -> Builtin.vec128.jkind
+      | "immutable_data" -> Builtin.immutable_data.jkind
+      | "mutable_data" -> Builtin.mutable_data.jkind
       | _ -> raise ~loc:jkind.pjkind_loc (Unknown_jkind jkind))
       |> allow_left |> allow_right
-    | Mod (jkind, modifiers) ->
-      let base = of_user_written_annotation_unchecked_level context jkind in
+    | Mod (base, modifiers) ->
+      let base = of_user_written_annotation_unchecked_level context base in
       (* for each mode, lower the corresponding modal bound to be that mode *)
       let parsed_modifiers = Typemode.transl_modifier_annots modifiers in
-      let parsed_modes : Alloc.Const.Option.t =
-        { areality = parsed_modifiers.locality;
-          linearity = parsed_modifiers.linearity;
-          uniqueness = parsed_modifiers.uniqueness;
-          portability = parsed_modifiers.portability;
-          contention = parsed_modifiers.contention
-        }
+      let upper_bounds =
+        Bounds.Create.f
+          { f =
+              (fun (type a) ~(axis : a Axis.t) : _ Bound.t ->
+                let (module A : Lattice with type t = a) = Axis.get axis in
+                let parsed_modifier =
+                  Typemode.Transled_modifiers.get ~axis parsed_modifiers
+                in
+                let base_bound = Bounds.get ~axis base.upper_bounds in
+                match parsed_modifier, base_bound with
+                | None, base_bound -> base_bound
+                | ( Some parsed_modifier,
+                    { modifier = base_modifier; baggage = No_baggage } ) ->
+                  { modifier = A.meet base_modifier parsed_modifier.txt;
+                    baggage = No_baggage
+                  }
+                | Some parsed_modifier, { modifier = _; baggage = Baggage _ } ->
+                  raise ~loc:parsed_modifier.loc
+                    (Modded_bound_with_baggage_constraints axis))
+          }
       in
-      { layout = base.layout;
-        modes_upper_bounds =
-          Alloc.Const.meet base.modes_upper_bounds
-            (Alloc.Const.Option.value ~default:Alloc.Const.max parsed_modes);
-        nullability_upper_bound =
-          Nullability.meet base.nullability_upper_bound
-            (Option.value ~default:Nullability.max parsed_modifiers.nullability);
-        externality_upper_bound =
-          Externality.meet base.externality_upper_bound
-            (Option.value ~default:Externality.max parsed_modifiers.externality)
-      }
+      { layout = base.layout; upper_bounds }
     | Product ts ->
       let jkinds =
         List.map (of_user_written_annotation_unchecked_level context) ts
       in
       jkind_of_product_annotations jkinds
-    | Default | With _ | Kind_of _ -> Misc.fatal_error "XXX unimplemented"
+    | With (base, type_) -> (
+      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
+        { layout = base.layout;
+          upper_bounds =
+            Bounds.add_baggage ~deep_only:true ~baggage:type_ base.upper_bounds
+        })
+    | Default | Kind_of _ -> Misc.fatal_error "XXX unimplemented"
 
   (* The [annotation_context] parameter can be used to allow annotations / kinds
      in different contexts to be enabled with different extension settings.
@@ -800,10 +1092,10 @@ module Const = struct
      parameter might effectively be unused.
   *)
   (* CR layouts: When everything is stable, remove this function. *)
-  let get_required_layouts_level (_context : 'd History.annotation_context)
+  let get_required_layouts_level (_context : 'd Context_with_transl.t)
       (jkind : 'd t) =
     let rec scan_layout (l : Layout.Const.t) : Language_extension.maturity =
-      match l, jkind.nullability_upper_bound with
+      match l, jkind.upper_bounds.nullability.modifier with
       | (Base (Float64 | Float32 | Word | Bits32 | Bits64 | Vec128) | Any), _
       | Base Value, Non_null ->
         Stable
@@ -826,7 +1118,7 @@ module Const = struct
 end
 
 module Desc = struct
-  type 'd t = (Sort.Flat.t Layout.t, 'd) Layout_and_axes.t
+  type 'd t = (type_expr, Sort.Flat.t Layout.t, 'd) Layout_and_axes.t
 
   let get_const t = Layout_and_axes.map_option Layout.get_flat_const t
 
@@ -835,8 +1127,7 @@ module Desc = struct
      algorithm. *)
   let format ppf t =
     let open Format in
-    let rec format_desc ~nested ppf
-        (desc : (Sort.Flat.t Layout.t, _) Layout_and_axes.t) =
+    let rec format_desc ~nested ppf (desc : _ t) =
       match desc.layout with
       | Sort (Var n) -> fprintf ppf "'s%d" (Sort.Var.get_print_number n)
       (* Analyze a product before calling [get_const]: the machinery in
@@ -859,77 +1150,72 @@ module Jkind_desc = struct
   let of_const t = Layout_and_axes.map Layout.of_const t
 
   let add_nullability_crossing t =
-    { t with nullability_upper_bound = Nullability.min }
+    { t with
+      upper_bounds =
+        { t.upper_bounds with nullability = Bound.simple Nullability.min }
+    }
 
-  let add_portability_and_contention_crossing ~from t =
-    let new_portability =
-      Portability.Const.meet t.modes_upper_bounds.portability
-        from.modes_upper_bounds.portability
+  let add_portability_and_contention_crossing ~type_equal ~jkind_of_type ~from
+      to_ =
+    let add_crossing (type a) ~(axis : a Axis.t) to_ =
+      let (module A : Lattice with type t = a) = Axis.get axis in
+      let from_bound = Bounds.get ~axis from.upper_bounds in
+      let to_bound = Bounds.get ~axis to_ in
+      let new_bound =
+        (* Only do this when the new mode is less than the old one. We
+           don't want to discard baggage if the new one is greater than
+           the old one. *)
+        if A.le from_bound.modifier to_bound.modifier
+           (* This discards any baggage, but that's what we want when doing illegal
+              crossing. *)
+        then Bound.simple from_bound.modifier
+        else to_bound
+      in
+      let added_crossings =
+        not
+          (Misc.Le_result.is_le
+             (Bound.less_or_equal ~axis ~type_equal ~jkind_of_type to_bound
+                from_bound))
+      in
+      Bounds.set ~axis to_ new_bound, added_crossings
     in
-    let new_contention =
-      Contention.Const.meet t.modes_upper_bounds.contention
-        from.modes_upper_bounds.contention
+    let upper_bounds = to_.upper_bounds in
+    let upper_bounds, added1 =
+      add_crossing ~axis:(Modal Portability) upper_bounds
     in
-    let added_crossings =
-      (not
-         (Portability.Const.le t.modes_upper_bounds.portability new_portability))
-      || not
-           (Contention.Const.le t.modes_upper_bounds.contention new_contention)
+    let upper_bounds, added2 =
+      add_crossing ~axis:(Modal Contention) upper_bounds
     in
-    ( { t with
-        modes_upper_bounds =
-          { t.modes_upper_bounds with
-            portability = new_portability;
-            contention = new_contention
-          }
-      },
-      added_crossings )
+    { to_ with upper_bounds }, added1 || added2
+
+  let add_baggage ~deep_only ~baggage t =
+    { t with
+      upper_bounds = Bounds.add_baggage ~deep_only ~baggage t.upper_bounds
+    }
 
   let max = of_const Const.max
 
-  let equate_or_equal ~allow_mutation
-      { layout = lay1;
-        modes_upper_bounds = modes1;
-        externality_upper_bound = ext1;
-        nullability_upper_bound = null1
-      }
-      { layout = lay2;
-        modes_upper_bounds = modes2;
-        externality_upper_bound = ext2;
-        nullability_upper_bound = null2
-      } =
-    Layout.equate_or_equal ~allow_mutation lay1 lay2
-    && Modes.equal modes1 modes2
-    && Externality.equal ext1 ext2
-    && Nullability.equal null1 null2
-
-  let sub t1 t2 = Layout_and_axes.sub Layout.sub t1 t2
-
-  let intersection
-      { layout = lay1;
-        modes_upper_bounds = modes1;
-        externality_upper_bound = ext1;
-        nullability_upper_bound = null1
-      }
-      { layout = lay2;
-        modes_upper_bounds = modes2;
-        externality_upper_bound = ext2;
-        nullability_upper_bound = null2
-      } =
-    Option.bind (Layout.intersection lay1 lay2) (fun layout ->
-        Some
-          { layout;
-            modes_upper_bounds = Modes.meet modes1 modes2;
-            externality_upper_bound = Externality.meet ext1 ext2;
-            nullability_upper_bound = Nullability.meet null1 null2
-          })
+  let equate_or_equal ~allow_mutation t1 t2 =
+    Layout_and_axes.equal (Layout.equate_or_equal ~allow_mutation) t1 t2
+
+  let sub ~type_equal ~jkind_of_type { layout = lay1; upper_bounds = bounds1 }
+      { layout = lay2; upper_bounds = bounds2 } =
+    Misc.Le_result.combine (Layout.sub lay1 lay2)
+      (Bounds.less_or_equal ~type_equal ~jkind_of_type bounds1 bounds2)
+
+  let intersection { layout = lay1; upper_bounds = bounds1 }
+      { layout = lay2; upper_bounds = bounds2 } =
+    match Layout.intersection lay1 lay2 with
+    | None -> None
+    | Some layout -> Some { layout; upper_bounds = Bounds.meet bounds1 bounds2 }
+
+  let map_type_expr f t = Layout_and_axes.map_type_expr f t
 
   let of_new_sort_var nullability_upper_bound =
     let layout, sort = Layout.of_new_sort_var () in
     ( { layout;
-        modes_upper_bounds = Modes.max;
-        externality_upper_bound = Externality.max;
-        nullability_upper_bound
+        upper_bounds =
+          { Bounds.max with nullability = Bound.simple nullability_upper_bound }
       },
       sort )
 
@@ -940,6 +1226,10 @@ module Jkind_desc = struct
 
     let value = of_const Const.Builtin.value.jkind
 
+    let immutable_data = of_const Const.Builtin.immutable_data.jkind
+
+    let mutable_data = of_const Const.Builtin.mutable_data.jkind
+
     let void = of_const Const.Builtin.void.jkind
 
     let immediate = of_const Const.Builtin.immediate.jkind
@@ -950,27 +1240,18 @@ module Jkind_desc = struct
        jkinds. This is not great. We should, as part of a broader pass on error
        messages around product kinds, zip them up into some kind of product
        history. *)
-    let folder (layouts, annotations, mode_ub, ext_ub, null_ub)
-        { jkind =
-            { layout;
-              modes_upper_bounds;
-              externality_upper_bound;
-              nullability_upper_bound
-            };
+    let folder (layouts, annotations, upper_bounds_acc)
+        { jkind = { layout; upper_bounds };
           annotation;
           history = _;
           has_warned = _
         } =
       ( layout :: layouts,
         annotation :: annotations,
-        Modes.join mode_ub modes_upper_bounds,
-        Externality.join ext_ub externality_upper_bound,
-        Nullability.join null_ub nullability_upper_bound )
+        Bounds.join upper_bounds upper_bounds_acc )
     in
-    let layouts, annotations, mode_ub, ext_ub, null_ub =
-      List.fold_left folder
-        ([], [], Modes.min, Externality.min, Nullability.min)
-        jkinds
+    let layouts, annotations, upper_bounds =
+      List.fold_left folder ([], [], Bounds.(min |> disallow_right)) jkinds
     in
     let layouts = List.rev layouts in
     let annotations = List.rev annotations in
@@ -982,12 +1263,7 @@ module Jkind_desc = struct
             { pjkind_loc = Location.none; pjkind_desc = Product annotations })
         annotations
     in
-    ( { layout : _ Layout.t = Product layouts;
-        modes_upper_bounds = mode_ub;
-        externality_upper_bound = ext_ub;
-        nullability_upper_bound = null_ub
-      },
-      annotation )
+    { layout : _ Layout.t = Product layouts; upper_bounds }, annotation
 
   let get t = Layout_and_axes.map Layout.get t
 
@@ -995,7 +1271,7 @@ module Jkind_desc = struct
 
   module Debug_printers = struct
     let t ppf t =
-      Layout_and_axes.format
+      Layout_and_axes.debug_print
         (Layout.Debug_printers.t Sort.Debug_printers.t)
         ppf t
   end
@@ -1020,7 +1296,9 @@ module Builtin = struct
   (* CR layouts: Should we be doing more memoization here? *)
   let any ~(why : History.any_creation_reason) =
     match why with
-    | Dummy_jkind -> any_dummy_jkind (* share this one common case *)
+    | Dummy_jkind ->
+      any_dummy_jkind (* share this one common case *) |> allow_left
+      |> allow_right
     | _ ->
       fresh_jkind Jkind_desc.Builtin.any ~annotation:(mk_annot "any")
         ~why:(Any_creation why)
@@ -1038,7 +1316,7 @@ module Builtin = struct
 
   let value_or_null ~why =
     match (why : History.value_or_null_creation_reason) with
-    | V1_safety_check -> value_v1_safety_check
+    | V1_safety_check -> value_v1_safety_check |> allow_left |> allow_right
     | _ ->
       fresh_jkind Jkind_desc.Builtin.value_or_null
         ~annotation:(mk_annot "value_or_null") ~why:(Value_or_null_creation why)
@@ -1047,6 +1325,15 @@ module Builtin = struct
     fresh_jkind Jkind_desc.Builtin.value ~annotation:(mk_annot "value")
       ~why:(Value_creation why)
 
+  let immutable_data ~(why : History.value_creation_reason) =
+    fresh_jkind Jkind_desc.Builtin.immutable_data
+      ~annotation:(mk_annot "immutable_data")
+      ~why:(Value_creation why)
+
+  let mutable_data ~(why : History.value_creation_reason) =
+    fresh_jkind Jkind_desc.Builtin.mutable_data
+      ~annotation:(mk_annot "mutable_data") ~why:(Value_creation why)
+
   let immediate ~why =
     fresh_jkind Jkind_desc.Builtin.immediate ~annotation:(mk_annot "immediate")
       ~why:(Immediate_creation why)
@@ -1057,17 +1344,26 @@ module Builtin = struct
     | [t] -> t
     | ts ->
       let desc, annotation = Jkind_desc.product ts in
-      fresh_jkind desc ~annotation ~why:(Product_creation why)
+      fresh_jkind_poly desc ~annotation ~why:(Product_creation why)
 end
 
 let add_nullability_crossing t =
   { t with jkind = Jkind_desc.add_nullability_crossing t.jkind }
 
-let add_portability_and_contention_crossing ~from t =
-  let jkind, added_crossings =
-    Jkind_desc.add_portability_and_contention_crossing ~from:from.jkind t.jkind
-  in
-  { t with jkind }, added_crossings
+let add_baggage ~baggage t =
+  { t with jkind = Jkind_desc.add_baggage ~deep_only:true ~baggage t.jkind }
+
+let has_baggage t = Bounds.has_baggage t.jkind.upper_bounds
+
+let add_portability_and_contention_crossing ~type_equal ~jkind_of_type ~from t =
+  match try_allow_r from with
+  | None -> t, false
+  | Some from ->
+    let jkind, added_crossings =
+      Jkind_desc.add_portability_and_contention_crossing ~type_equal
+        ~jkind_of_type ~from:from.jkind t.jkind
+    in
+    { t with jkind }, added_crossings
 
 (******************************)
 (* construction *)
@@ -1084,55 +1380,50 @@ let of_new_legacy_sort_var ~why =
 
 let of_new_legacy_sort ~why = fst (of_new_legacy_sort_var ~why)
 
-let of_const ~annotation ~why
-    ({ layout;
-       modes_upper_bounds;
-       externality_upper_bound;
-       nullability_upper_bound
-     } :
-      'd Const.t) =
-  { jkind =
-      { layout = Layout.of_const layout;
-        modes_upper_bounds;
-        externality_upper_bound;
-        nullability_upper_bound
-      };
+let of_const ~annotation ~why (c : 'd Const.t) =
+  { jkind = Layout_and_axes.map Layout.of_const c;
     annotation;
     history = Creation why;
     has_warned = false
   }
 
 let of_builtin ~why Const.Builtin.{ jkind; name } =
-  of_const ~annotation:(mk_annot name) ~why jkind
+  of_const ~annotation:(mk_annot name) ~why jkind |> allow_left |> allow_right
 
 let of_annotated_const ~context ~annotation ~const ~const_loc =
+  let context = Context_with_transl.get_context context in
   of_const ~annotation ~why:(Annotated (context, const_loc)) const
 
-let of_annotation ~context (annot : Parsetree.jkind_annotation) =
+let of_annotation_lr ~context (annot : Parsetree.jkind_annotation) =
   let const = Const.of_user_written_annotation ~context annot in
   of_annotated_const ~annotation:(Some annot) ~const ~const_loc:annot.pjkind_loc
     ~context
 
+let of_annotation ~context annot =
+  of_annotation_lr ~context:(Right_jkind context) annot
+
 let of_annotation_option_default ~default ~context = function
   | None -> default
   | Some annot -> of_annotation ~context annot
 
 let of_attribute ~context
     (attribute : Builtin_attributes.jkind_attribute Location.loc) =
-  let ({ jkind = const; name } : _ Const.Builtin.t) =
+  let ({ jkind = const; name } : Const.Builtin.t) =
     Const.Builtin.of_attribute attribute.txt
   in
   of_annotated_const ~context ~annotation:(mk_annot name) ~const
     ~const_loc:attribute.loc
 
-let of_type_decl ~context (decl : Parsetree.type_declaration) =
+let of_type_decl ~context ~transl_type (decl : Parsetree.type_declaration) =
+  let context = Context_with_transl.Left_jkind (transl_type, context) in
   let jkind_of_annotation =
     decl.ptype_jkind_annotation
-    |> Option.map (fun annot -> of_annotation ~context annot, annot)
+    |> Option.map (fun annot -> of_annotation_lr ~context annot, annot)
   in
   let jkind_of_attribute =
     Builtin_attributes.jkind decl.ptype_attributes
-    |> Option.map (fun attr -> (of_attribute ~context attr, None), attr)
+    |> Option.map (fun attr ->
+           (of_attribute ~context attr |> disallow_right, None), attr)
   in
   match jkind_of_annotation, jkind_of_attribute with
   | None, None -> None
@@ -1142,47 +1433,112 @@ let of_type_decl ~context (decl : Parsetree.type_declaration) =
     raise ~loc:decl.ptype_loc
       (Multiple_jkinds { from_annotation; from_attribute })
 
-let of_type_decl_default ~context ~default (decl : Parsetree.type_declaration) =
-  match of_type_decl ~context decl with Some (t, _) -> t | None -> default
+let of_type_decl_default ~context ~transl_type ~default
+    (decl : Parsetree.type_declaration) =
+  match of_type_decl ~context ~transl_type decl with
+  | Some (t, _) -> t
+  | None -> default
 
-let for_boxed_record ~all_void =
-  if all_void
+let has_mutable_label lbls =
+  List.exists
+    (fun (lbl : Types.label_declaration) ->
+      match lbl.ld_mutable with Immutable -> false | Mutable _ -> true)
+    lbls
+
+let all_void_labels lbls =
+  List.for_all
+    (fun (lbl : Types.label_declaration) -> Sort.Const.(equal void lbl.ld_sort))
+    lbls
+
+let add_labels_as_baggage lbls jkind =
+  List.fold_right
+    (fun (lbl : Types.label_declaration) -> add_baggage ~baggage:lbl.ld_type)
+    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
-  else Builtin.value ~why:Boxed_record
-
-let for_boxed_variant ~all_voids =
-  if all_voids
+  else
+    let is_mutable = has_mutable_label lbls in
+    let base =
+      (if is_mutable then Builtin.mutable_data else Builtin.immutable_data)
+        ~why:Boxed_record
+    in
+    add_labels_as_baggage lbls base
+
+(* CR layouts v2.8: This should take modalities into account. *)
+let for_boxed_variant cstrs =
+  let open Types in
+  if List.for_all
+       (fun cstr ->
+         match cstr.cd_args with
+         | Cstr_tuple args ->
+           List.for_all (fun arg -> Sort.Const.(equal void arg.ca_sort)) args
+         | Cstr_record lbls -> all_void_labels lbls)
+       cstrs
   then Builtin.immediate ~why:Enumeration
-  else Builtin.value ~why:Boxed_variant
+  else
+    let is_mutable =
+      List.exists
+        (fun cstr ->
+          match cstr.cd_args with
+          | Cstr_tuple _ -> false
+          | Cstr_record lbls -> has_mutable_label lbls)
+        cstrs
+    in
+    let has_gadt_constructor =
+      List.exists
+        (fun cstr -> match cstr.cd_res with None -> false | Some _ -> true)
+        cstrs
+    in
+    if has_gadt_constructor
+       (* CR layouts v2.8: This is sad, but I don't know how to account for
+          existentials in the baggage. See doc named "Existential
+          baggage". *)
+    then Builtin.value ~why:Boxed_variant
+    else
+      let base =
+        (if is_mutable then Builtin.mutable_data else Builtin.immutable_data)
+          ~why:Boxed_variant
+      in
+      let add_cstr_args cstr jkind =
+        match cstr.cd_args with
+        | Cstr_tuple args ->
+          List.fold_right
+            (fun arg -> add_baggage ~baggage:arg.ca_type)
+            args jkind
+        | Cstr_record lbls -> add_labels_as_baggage lbls jkind
+      in
+      List.fold_right add_cstr_args cstrs base
 
 let for_arrow =
   fresh_jkind
     { layout = Sort (Base Value);
-      modes_upper_bounds =
-        { linearity = Linearity.Const.max;
-          areality = Locality.Const.max;
-          uniqueness = Uniqueness.Const.min;
-          portability = Portability.Const.max;
-          contention = Contention.Const.min
-        };
-      externality_upper_bound = Externality.max;
-      nullability_upper_bound = Non_null
+      upper_bounds =
+        Bounds.simple ~linearity:Linearity.Const.max
+          ~locality:Locality.Const.max ~uniqueness:Uniqueness.Const.min
+          ~portability:Portability.Const.max ~contention:Contention.Const.min
+          ~externality:Externality.max ~nullability:Nullability.Non_null
     }
     ~annotation:None ~why:(Value_creation Arrow)
 
 let for_object =
+  let ({ linearity; areality = locality; uniqueness; portability; contention }
+        : Mode.Alloc.Const.t) =
+    (* The crossing of objects are based on the fact that they are
+       produced/defined/allocated at legacy, which applies to only the
+       comonadic axes. *)
+    Alloc.Const.merge
+      { comonadic = Alloc.Comonadic.Const.legacy;
+        monadic = Alloc.Monadic.Const.max
+      }
+  in
   fresh_jkind
     { layout = Sort (Base Value);
-      modes_upper_bounds =
-        (* The crossing of objects are based on the fact that they are
-           produced/defined/allocated at legacy, which applies to only the
-           comonadic axes. *)
-        Alloc.Const.merge
-          { comonadic = Alloc.Comonadic.Const.legacy;
-            monadic = Alloc.Monadic.Const.max
-          };
-      externality_upper_bound = Externality.max;
-      nullability_upper_bound = Non_null
+      upper_bounds =
+        Bounds.simple ~linearity ~locality ~uniqueness ~portability ~contention
+          ~externality:Externality.max ~nullability:Non_null
     }
     ~annotation:None ~why:(Value_creation Object)
 
@@ -1211,12 +1567,39 @@ let sort_of_jkind (t : jkind_l) : sort =
 
 let get_layout jk : Layout.Const.t option = Layout.get_const jk.jkind.layout
 
-let get_modal_upper_bounds jk = jk.jkind.modes_upper_bounds
+let get_modal_upper_bounds ~type_equal ~jkind_of_type jk : Alloc.Const.t =
+  let bounds = jk.jkind.upper_bounds in
+  { areality =
+      Bound.reduce ~axis:(Modal Locality) ~type_equal ~jkind_of_type
+        bounds.locality;
+    linearity =
+      Bound.reduce ~axis:(Modal Linearity) ~type_equal ~jkind_of_type
+        bounds.linearity;
+    uniqueness =
+      Bound.reduce ~axis:(Modal Uniqueness) ~type_equal ~jkind_of_type
+        bounds.uniqueness;
+    portability =
+      Bound.reduce ~axis:(Modal Portability) ~type_equal ~jkind_of_type
+        bounds.portability;
+    contention =
+      Bound.reduce ~axis:(Modal Contention) ~type_equal ~jkind_of_type
+        bounds.contention
+  }
 
-let get_externality_upper_bound jk = jk.jkind.externality_upper_bound
+let get_externality_upper_bound ~type_equal ~jkind_of_type jk =
+  Bound.reduce ~axis:(Nonmodal Externality) ~type_equal ~jkind_of_type
+    jk.jkind.upper_bounds.externality
 
 let set_externality_upper_bound jk externality_upper_bound =
-  { jk with jkind = { jk.jkind with externality_upper_bound } }
+  { jk with
+    jkind =
+      { jk.jkind with
+        upper_bounds =
+          { jk.jkind.upper_bounds with
+            externality = Bound.simple externality_upper_bound
+          }
+      }
+  }
 
 let get_annotation jk = jk.annotation
 
@@ -1599,7 +1982,7 @@ module Violation = struct
   open Format
 
   type violation =
-    | Not_a_subjkind : (allowed * 'r) t * ('l * allowed) t -> violation
+    | Not_a_subjkind : (allowed * 'r1) t * ('l * 'r2) t -> violation
     | No_intersection : 'd t * ('l * allowed) t -> violation
 
   type nonrec t =
@@ -1731,8 +2114,6 @@ let equate_or_equal ~allow_mutation
 (* CR layouts v2.8: Switch this back to ~allow_mutation:false *)
 let equal t1 t2 = equate_or_equal ~allow_mutation:true t1 t2
 
-let () = Types.set_jkind_equal equal
-
 let equate t1 t2 = equate_or_equal ~allow_mutation:true t1 t2
 
 (* Not all jkind history reasons are created equal. Some are more helpful than others.
@@ -1747,7 +2128,7 @@ let score_reason = function
   | Creation (Concrete_creation _ | Concrete_legacy_creation _) -> -1
   | _ -> 0
 
-let combine_histories reason (Pack k1) (Pack k2) =
+let combine_histories ~type_equal ~jkind_of_type reason (Pack k1) (Pack k2) =
   if flattened_histories
   then
     let choose_higher_scored_history history_a history_b =
@@ -1756,7 +2137,7 @@ let combine_histories reason (Pack k1) (Pack k2) =
       else history_b
     in
     let choose_subjkind_history k_a history_a k_b history_b =
-      match Jkind_desc.sub k_a k_b with
+      match Jkind_desc.sub ~type_equal ~jkind_of_type k_a k_b with
       | Less -> history_a
       | Not_le ->
         (* CR layouts: this will be wrong if we ever have a non-trivial meet in
@@ -1782,59 +2163,113 @@ let combine_histories reason (Pack k1) (Pack k2) =
       }
 
 let has_intersection t1 t2 =
-  Option.is_some (Jkind_desc.intersection t1.jkind t2.jkind)
+  (* Need to check only the layouts: all the axes have bottom elements. *)
+  Option.is_some (Layout.intersection t1.jkind.layout t2.jkind.layout)
 
-let intersection_or_error ~reason t1 t2 =
+let intersection_or_error ~type_equal ~jkind_of_type ~reason t1 t2 =
   match Jkind_desc.intersection t1.jkind t2.jkind with
   | None -> Error (Violation.of_ (No_intersection (t1, t2)))
   | Some jkind ->
     Ok
       { jkind;
         annotation = None;
-        history = combine_histories reason (Pack t1) (Pack t2);
+        history =
+          combine_histories ~type_equal ~jkind_of_type reason (Pack t1)
+            (Pack t2);
         has_warned = t1.has_warned || t2.has_warned
       }
 
-let intersect_l_l ~reason t1 t2 =
-  (* CR layouts v2.8: Do something cleverer here once we have more
-     expressive l-kinds. *)
-  intersection_or_error ~reason t1 (terrible_relax_l t2)
+let round_up ~type_equal ~jkind_of_type t =
+  let upper_bounds =
+    Bounds.Map.f
+      { f =
+          (fun ~axis bound ->
+            Bound.simple (Bound.reduce ~axis ~type_equal ~jkind_of_type bound))
+      }
+      t.jkind.upper_bounds
+  in
+  { t with jkind = { t.jkind with upper_bounds } }
 
-let has_intersection_l_l t1 t2 =
-  (* CR layouts v2.8: Do something cleverer here once we have more
-     expressive l-kinds. *)
-  has_intersection (terrible_relax_l t1) (terrible_relax_l t2)
+let map_type_expr f t = { t with jkind = Jkind_desc.map_type_expr f t.jkind }
 
 (* this is hammered on; it must be fast! *)
-let check_sub sub super = Jkind_desc.sub sub.jkind super.jkind
+let check_sub ~jkind_of_type sub super =
+  Jkind_desc.sub ~jkind_of_type sub.jkind super.jkind
 
-let sub sub super = Misc.Le_result.is_le (check_sub sub super)
+let sub ~type_equal ~jkind_of_type sub super =
+  Misc.Le_result.is_le (check_sub ~type_equal ~jkind_of_type sub super)
 
 type sub_or_intersect =
   | Sub
   | Disjoint
   | Has_intersection
 
-let sub_or_intersect t1 t2 =
-  if sub t1 t2
+let sub_or_intersect ~type_equal ~jkind_of_type t1 t2 =
+  if sub ~type_equal ~jkind_of_type t1 t2
   then Sub
   else if has_intersection t1 t2
   then Has_intersection
   else Disjoint
 
-let sub_or_error t1 t2 =
-  match sub_or_intersect t1 t2 with
+let sub_or_error ~type_equal ~jkind_of_type t1 t2 =
+  match sub_or_intersect ~type_equal ~jkind_of_type t1 t2 with
   | Sub -> Ok ()
   | _ -> Error (Violation.of_ (Not_a_subjkind (t1, t2)))
 
 (* CR layouts v2.8: Rewrite this to do the hard subjkind check from the
    kind polymorphism design. *)
-let sub_jkind_l sub super =
-  let super = terrible_relax_l super in
-  match check_sub sub super with
-  | Less | Equal ->
-    Ok { sub with history = combine_histories Subjkind (Pack sub) (Pack super) }
-  | Not_le -> Error (Violation.of_ (Not_a_subjkind (sub, super)))
+let sub_jkind_l ~type_equal ~jkind_of_type sub super =
+  let success =
+    Ok
+      { sub with
+        history =
+          combine_histories ~type_equal ~jkind_of_type Subjkind (Pack sub)
+            (Pack super)
+      }
+  in
+  let failure = Error (Violation.of_ (Not_a_subjkind (sub, super))) in
+  (* First try normal subjkinding, if the right-hand jkind has the right
+     shape. *)
+  match try_allow_r super with
+  | Some super -> (
+    match check_sub ~type_equal ~jkind_of_type sub super with
+    | Less | Equal -> success
+    | Not_le -> failure)
+  | None ->
+    (* CR layouts v2.8: Do something better than just comparing for equality. *)
+    (* We can't use other functions, because they insist that we only compare
+       lr-jkinds for equality, not just l-jkinds. *)
+    let layouts =
+      Misc.Le_result.is_le (Layout.sub sub.jkind.layout super.jkind.layout)
+    in
+    let bounds =
+      Bounds.Fold2.f
+        { f =
+            (fun (type axis) ~(axis : axis Axis.t) (bound1 : _ Bound.t)
+                 (bound2 : _ Bound.t) ->
+              (* Maybe an individual axis has the right shape on the right;
+                 try this again before doing the stupid equality check. *)
+              match Bound.try_allow_r bound2 with
+              | Some bound2 ->
+                Misc.Le_result.is_le
+                  (Bound.less_or_equal ~axis ~type_equal ~jkind_of_type bound1
+                     bound2)
+              | None ->
+                let (module Bound_ops) = Axis.get axis in
+                let baggage1 = Baggage.as_list bound1.baggage in
+                let baggage2 = Baggage.as_list bound2.baggage in
+                let modifiers =
+                  Bound_ops.equal bound1.modifier bound2.modifier
+                in
+                let baggages =
+                  List.compare_lengths baggage1 baggage2 = 0
+                  && List.for_all2 type_equal baggage1 baggage2
+                in
+                modifiers && baggages)
+        }
+        ~combine:( && ) sub.jkind.upper_bounds super.jkind.upper_bounds
+    in
+    if layouts && bounds then success else failure
 
 let is_void_defaulting = function
   | { jkind = { layout = Sort s; _ }; _ } -> Sort.is_void_defaulting s
@@ -1842,32 +2277,37 @@ let is_void_defaulting = function
 
 (* This doesn't do any mutation because mutating a sort variable can't make it
    any, and modal upper bounds are constant. *)
-let is_max jkind = sub Builtin.any_dummy_jkind jkind
+(* The choice of [type_equal] and [jkind_of_type] doesn't matter because there
+   are no with-kinds on the left-hand kind. *)
+let is_max jkind =
+  sub
+    ~type_equal:(fun _ _ -> false)
+    ~jkind_of_type:(fun _ -> None)
+    Builtin.any_dummy_jkind jkind
 
 let has_layout_any jkind =
   match jkind.jkind.layout with Any -> true | _ -> false
 
-let is_value_for_printing
-    { jkind =
-        { layout;
-          modes_upper_bounds;
-          externality_upper_bound;
-          nullability_upper_bound
-        };
-      _
-    } =
-  match Layout.get_const layout with
+let is_value_for_printing { jkind; _ } =
+  match Desc.get_const (Jkind_desc.get jkind) with
+  | None -> false
   | Some const ->
     let value = Const.Builtin.value.jkind in
-    Layout.Const.equal const value.layout
-    && Modes.equal modes_upper_bounds value.modes_upper_bounds
-    && Externality.equal externality_upper_bound value.externality_upper_bound
-    &&
-    if (* CR layouts v3.0: remove this hack once [or_null] is out of [Alpha]. *)
-       Language_extension.(is_at_least Layouts Alpha)
-    then Nullability.equal nullability_upper_bound Nullability.Non_null
-    else true
-  | None -> false
+    let values = [value] in
+    let values =
+      if (* CR layouts v3.0: remove this hack once [or_null] is out of [Alpha]. *)
+         Language_extension.(is_at_least Layouts Alpha)
+      then values
+      else
+        { value with
+          upper_bounds =
+            { value.upper_bounds with
+              nullability = Bound.simple Nullability.Maybe_null
+            }
+        }
+        :: values
+    in
+    List.exists (fun v -> Const.no_baggage_and_equal const v) values
 
 (*********************************)
 (* debugging *)
@@ -2027,7 +2467,9 @@ module Debug_printers = struct
       fprintf ppf "Tyvar_refinement_intersection"
     | Subjkind -> fprintf ppf "Subjkind"
 
-  let rec history ppf = function
+  let rec history ~print_type_expr ppf =
+    let jkind_desc = Jkind_desc.Debug_printers.t ~print_type_expr in
+    function
     | Interact
         { reason;
           jkind1 = Pack jkind1;
@@ -2038,28 +2480,24 @@ module Debug_printers = struct
       fprintf ppf
         "Interact {@[reason = %a;@ jkind1 = %a;@ history1 = %a;@ jkind2 = %a;@ \
          history2 = %a}@]"
-        interact_reason reason Jkind_desc.Debug_printers.t jkind1 history
-        history1 Jkind_desc.Debug_printers.t jkind2 history history2
+        interact_reason reason jkind_desc jkind1 (history ~print_type_expr)
+        history1 jkind_desc jkind2 (history ~print_type_expr) history2
     | Creation c -> fprintf ppf "Creation (%a)" creation_reason c
 
-  let t ppf ({ jkind; annotation = a; history = h; has_warned = _ } : 'd t) :
-      unit =
+  let t ~print_type_expr ppf
+      ({ jkind; annotation = a; history = h; has_warned = _ } : 'd t) : unit =
     fprintf ppf "@[<v 2>{ jkind = %a@,; annotation = %a@,; history = %a }@]"
-      Jkind_desc.Debug_printers.t jkind
+      (Jkind_desc.Debug_printers.t ~print_type_expr)
+      jkind
       (pp_print_option Pprintast.jkind_annotation)
-      a history h
+      a (history ~print_type_expr) h
 
   module Const = struct
-    let t ppf (jkind : _ Const.t) =
-      fprintf ppf
-        "@[<v 2>{ layout = %a@,\
-         ; modes_upper_bounds = %a@,\
-         ; externality_upper_bound = %a@,\
-         ; nullability_upper_bound = %a@,\
-         }@]"
-        Layout.Const.Debug_printers.t jkind.layout Modes.print
-        jkind.modes_upper_bounds Externality.print jkind.externality_upper_bound
-        Nullability.print jkind.nullability_upper_bound
+    let t ~print_type_expr ppf (jkind : _ Const.t) =
+      fprintf ppf "@[<v 2>{ layout = %a@,; modes_upper_bounds = %a@,}@]"
+        Layout.Const.Debug_printers.t jkind.layout
+        (Bounds.debug_print ~print_type_expr)
+        jkind.upper_bounds
   end
 end
 
@@ -2097,6 +2535,13 @@ let report_error ~loc : Error.t -> _ = function
          layouts extension.@;\
          %t@]"
         Pprintast.jkind_annotation jkind hint)
+  | Modded_bound_with_baggage_constraints axis ->
+    Location.errorf ~loc
+      "Attempted to 'mod' a kind along the %s axis, which has already been \
+       constrained with a 'with' constraint."
+      (Axis.name axis)
+  | With_on_right ->
+    Location.errorf ~loc "'with' syntax is not allowed on a right mode."
 
 let () =
   Location.register_error_of_exn (function
diff --git a/typing/jkind.mli b/typing/jkind.mli
index aa6bf5ab3ce..af4c60c1772 100644
--- a/typing/jkind.mli
+++ b/typing/jkind.mli
@@ -113,7 +113,7 @@ end
     the meets (intersections) of r-jkinds and check that an l-jkind is less
     than an r-jkind.
 *)
-type +'d t = (Types.type_expr, 'd) Jkind_types.t
+type 'd t = (Types.type_expr, 'd) Jkind_types.t
 
 type jkind_l := Types.jkind_l
 
@@ -125,9 +125,8 @@ type packed = Pack : 'd t -> packed [@@unboxed]
 
 include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd t
 
-(** Convert an [l] into any jkind. This will soon become impossible, and so
-    uses of this function will have to be removed. *)
-val terrible_relax_l : jkind_l -> 'd t
+(** Try to treat this jkind as an r-jkind. *)
+val try_allow_r : ('l * 'r) t -> ('l * allowed) t option
 
 module History : sig
   include module type of struct
@@ -152,7 +151,10 @@ end
 
 module Violation : sig
   type violation =
-    | Not_a_subjkind : (allowed * 'r) t * ('l * allowed) t -> violation
+    (* [Not_a_subjkind] allows l-jkinds on the right so that it can be used
+       in [sub_jkind_l]. There is no downside to this, as the printing
+       machinery works over l-jkinds. *)
+    | Not_a_subjkind : (allowed * 'r1) t * ('l * 'r2) t -> violation
     | No_intersection : 'd t * ('l * allowed) t -> violation
 
   type t
@@ -197,80 +199,81 @@ module Const : sig
       The "constant" refers to the fact that there are no sort variables here.
       The existence of [with]-types means, though, that we still need the
       allowance machinery here. *)
-  type +'d t constraint 'd = 'l * 'r
+  type 'd t constraint 'd = 'l * 'r
 
   val to_out_jkind_const : 'd t -> Outcometree.out_jkind_const
 
-  (* An equality check should work over [lr]s only. But we need this
-     to do memoization in serialization. Happily, that's after all
-     inference is done, when worrying about l and r does not matter
-     any more. *)
-  val equal_after_all_inference_is_done : 'd1 t -> 'd2 t -> bool
+  (** This returns [true] iff both types have no baggage and they are equal.
+      Normally, we want an equality check to happen only on values that are
+      allowed on both the left and the right. But a type with no baggage is
+      allowed on the left and the right, so we test for that condition first
+      before doing the proper equality check. *)
+  val no_baggage_and_equal : 'd1 t -> 'd2 t -> bool
 
   (* CR layouts: Remove this once we have a better story for printing with jkind
      abbreviations. *)
   module Builtin : sig
-    type nonrec 'd t =
-      { jkind : 'd t;
+    type nonrec t =
+      { jkind : (allowed * allowed) t;
         name : string
       }
 
     (** This jkind is the top of the jkind lattice. All types have jkind [any].
     But we cannot compile run-time manipulations of values of types with jkind
     [any]. *)
-    val any : 'd t
+    val any : t
 
     (** [any], except for null pointers. *)
-    val any_non_null : 'd t
+    val any_non_null : t
 
     (** Value of types of this jkind are not retained at all at runtime *)
-    val void : 'd t
+    val void : t
 
     (** This is the jkind of normal ocaml values or null pointers *)
-    val value_or_null : 'd t
+    val value_or_null : t
 
     (** This is the jkind of normal ocaml values *)
-    val value : 'd t
+    val value : t
 
     (** Immutable values that don't contain functions. *)
-    val immutable_data : 'd t
+    val immutable_data : t
 
     (** Mutable values that don't contain functions. *)
-    val mutable_data : 'd t
+    val mutable_data : t
 
     (** Values of types of this jkind are immediate on 64-bit platforms; on other
     platforms, we know nothing other than that it's a value. *)
-    val immediate64 : 'd t
+    val immediate64 : t
 
     (** We know for sure that values of types of this jkind are always immediate *)
-    val immediate : 'd t
+    val immediate : t
 
     (** This is the jkind of unboxed 64-bit floats.  They have sort
     Float64. Mode-crosses. *)
-    val float64 : 'd t
+    val float64 : t
 
     (** This is the jkind of unboxed 32-bit floats.  They have sort
     Float32. Mode-crosses. *)
-    val float32 : 'd t
+    val float32 : t
 
     (** This is the jkind of unboxed native-sized integers. They have sort
     Word. Does not mode-cross. *)
-    val word : 'd t
+    val word : t
 
     (** This is the jkind of unboxed 32-bit integers. They have sort Bits32. Does
     not mode-cross. *)
-    val bits32 : 'd t
+    val bits32 : t
 
     (** This is the jkind of unboxed 64-bit integers. They have sort Bits64. Does
     not mode-cross. *)
-    val bits64 : 'd t
+    val bits64 : t
 
     (** This is the jkind of unboxed 128-bit simd vectors. They have sort Vec128. Does
     not mode-cross. *)
-    val vec128 : 'd t
+    val vec128 : t
 
     (** A list of all Builtin jkinds *)
-    val all : 'd t list
+    val all : t list
   end
 end
 
@@ -288,6 +291,12 @@ module Builtin : sig
   (** This is the jkind of normal ocaml values *)
   val value : why:History.value_creation_reason -> 'd t
 
+  (** This is suitable for records or variants without mutable fields. *)
+  val immutable_data : why:History.value_creation_reason -> 'd t
+
+  (** This is suitable for records or variants with mutable fields. *)
+  val mutable_data : why:History.value_creation_reason -> 'd t
+
   (** We know for sure that values of types of this jkind are always immediate *)
   val immediate : why:History.immediate_creation_reason -> 'd t
 
@@ -297,17 +306,30 @@ module Builtin : sig
       - If two or more input kinds are given, then the layout will be the
         product of the layouts of the input kinds, and the other components of
         the kind will be the join relevant component of the inputs.
-  *)
-  val product : why:History.product_creation_reason -> 'd t list -> 'd t
+
+      This is defined to work only on [jkind_l] simply as a matter of
+      convenience; it can be generalized if need be.  *)
+  val product : why:History.product_creation_reason -> jkind_l list -> jkind_l
 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
+
+(** Does this jkind have baggage? *)
+val has_baggage : jkind_l -> bool
+
 (** Take an existing [t] and add an ability to mode-cross along the portability and
     contention axes, if [from] crosses the respective axes. Return the new jkind,
     along with a boolean of whether illegal crossing was added *)
-val add_portability_and_contention_crossing : from:'d t -> 'd t -> 'd t * bool
+val add_portability_and_contention_crossing :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  from:'d t ->
+  (allowed * 'r) t ->
+  (allowed * 'r) t * bool
 
 (******************************)
 (* construction *)
@@ -336,18 +358,18 @@ val of_const :
   'd Const.t ->
   'd t
 
-val of_builtin : why:History.creation_reason -> 'd Const.Builtin.t -> 'd t
-
-(* CR layouts v2.8: remove this when printing is improved *)
+val of_builtin : why:History.creation_reason -> Const.Builtin.t -> 'd t
 
 val of_annotation :
-  context:'d History.annotation_context -> Parsetree.jkind_annotation -> 'd t
+  context:('l * allowed) History.annotation_context ->
+  Parsetree.jkind_annotation ->
+  ('l * allowed) t
 
 val of_annotation_option_default :
-  default:'d t ->
-  context:'d History.annotation_context ->
+  default:('l * allowed) t ->
+  context:('l * allowed) History.annotation_context ->
   Parsetree.jkind_annotation option ->
-  'd t
+  ('l * allowed) t
 
 (** Find a jkind from a type declaration. Type declarations are special because
     the jkind may have been provided via [: jkind] syntax (which goes through
@@ -361,6 +383,7 @@ val of_annotation_option_default :
 *)
 val of_type_decl :
   context:History.annotation_context_l ->
+  transl_type:(Parsetree.core_type -> Types.type_expr) ->
   Parsetree.type_declaration ->
   (jkind_l * Parsetree.jkind_annotation option) option
 
@@ -371,17 +394,16 @@ val of_type_decl :
 *)
 val of_type_decl_default :
   context:History.annotation_context_l ->
+  transl_type:(Parsetree.core_type -> Types.type_expr) ->
   default:jkind_l ->
   Parsetree.type_declaration ->
   jkind_l
 
-(** Choose an appropriate jkind for a boxed record type, given whether
-    all of its fields are [void]. *)
-val for_boxed_record : all_void:bool -> jkind_l
+(** Choose an appropriate jkind for a boxed record type *)
+val for_boxed_record : Types.label_declaration list -> jkind_l
 
-(** Choose an appropriate jkind for a boxed variant type, given whether
-    all of the fields of all of its constructors are [void]. *)
-val for_boxed_variant : all_voids:bool -> jkind_l
+(** Choose an appropriate jkind for a boxed variant type. *)
+val for_boxed_variant : Types.constructor_declaration list -> jkind_l
 
 (** The jkind of an arrow type. *)
 val for_arrow : jkind_l
@@ -396,7 +418,8 @@ module Desc : sig
   (** The description of a jkind, used as a return type from [get].  This
       description has no sort variables, but it might have [with]-types and thus
       needs the allowance machinery. *)
-  type 'd t = (Sort.Flat.t Layout.t, 'd) Jkind_types.Layout_and_axes.t
+  type 'd t =
+    (Types.type_expr, Sort.Flat.t Layout.t, 'd) Jkind_types.Layout_and_axes.t
 
   val get_const : 'd t -> 'd Const.t option
 
@@ -432,14 +455,19 @@ val sort_of_jkind : jkind_l -> sort
     Never does mutation. *)
 val get_layout : 'd t -> Layout.Const.t option
 
-(* CR layouts v2.8: This will need to become significantly more involved with
-   [with]-types. *)
-
 (** Gets the maximum modes for types of this jkind. *)
-val get_modal_upper_bounds : 'd t -> Mode.Alloc.Const.t
+val get_modal_upper_bounds :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  'd t ->
+  Mode.Alloc.Const.t
 
 (** Gets the maximum mode on the externality axis for types of this jkind. *)
-val get_externality_upper_bound : 'd t -> Externality.t
+val get_externality_upper_bound :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  'd t ->
+  Externality.t
 
 (** Computes a jkind that is the same as the input but with an updated maximum
     mode for the externality axis *)
@@ -459,6 +487,9 @@ val get_annotation : 'd t -> Parsetree.jkind_annotation option
 (*********************************)
 (* pretty printing *)
 
+(** Call this before trying to print. *)
+val set_print_type_expr : (Format.formatter -> Types.type_expr -> unit) -> unit
+
 val format : Format.formatter -> 'd t -> unit
 
 (** Format the history of this jkind: what interactions it has had and why
@@ -489,14 +520,10 @@ val equate : jkind_lr -> jkind_lr -> bool
 val equal : jkind_lr -> jkind_lr -> bool
 
 (** Checks whether two jkinds have a non-empty intersection. Might mutate
-    sort variables. *)
-val has_intersection : jkind_r -> jkind_r -> bool
-
-(* CR layouts v2.8: This almost certainly has to get rewritten, as l-kinds do
-   not support meets. *)
-
-(** Like [has_intersection], but comparing two [l] jkinds. *)
-val has_intersection_l_l : jkind_l -> jkind_l -> bool
+    sort variables. Works over any mix of l- and r-jkinds, because the only
+    way not to have an intersection is by looking at the layout: all axes
+    have a bottom element. *)
+val has_intersection : 'd1 t -> 'd2 t -> bool
 
 (** Finds the intersection of two jkinds, constraining sort variables to
     create one if needed, or returns a [Violation.t] if an intersection does
@@ -506,6 +533,8 @@ val has_intersection_l_l : jkind_l -> jkind_l -> bool
     it should be thought of as modifying the first jkind to be the
     intersection of the two, not something that modifies the second jkind. *)
 val intersection_or_error :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
   reason:History.interact_reason ->
   ('l1 * allowed) t ->
   ('l2 * allowed) t ->
@@ -513,7 +542,12 @@ val intersection_or_error :
 
 (** [sub t1 t2] says whether [t1] is a subjkind of [t2]. Might update
     either [t1] or [t2] to make their layouts equal.*)
-val sub : jkind_l -> jkind_r -> bool
+val sub :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  jkind_l ->
+  jkind_r ->
+  bool
 
 type sub_or_intersect =
   | Sub  (** The first jkind is a subjkind of the second. *)
@@ -522,27 +556,49 @@ type sub_or_intersect =
 
 (** [sub_or_intersect t1 t2] does a subtype check, returning a [sub_or_intersect];
     see comments there for more info. *)
-val sub_or_intersect : (allowed * 'r) t -> ('l * allowed) t -> sub_or_intersect
+val sub_or_intersect :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  (allowed * 'r) t ->
+  ('l * allowed) t ->
+  sub_or_intersect
 
 (** [sub_or_error t1 t2] does a subtype check, returning an appropriate
     [Violation.t] upon failure. *)
-val sub_or_error : jkind_l -> jkind_r -> (unit, Violation.t) result
+val sub_or_error :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  (allowed * 'r) t ->
+  ('l * allowed) t ->
+  (unit, Violation.t) result
 
 (** Like [sub], but returns the subjkind with an updated history.
-    Pre-condition: the super jkind must be fully settled; no variables
-    which might be filled in later. *)
-val sub_jkind_l : jkind_l -> jkind_l -> (jkind_l, Violation.t) result
-
-(* CR layouts v2.8: This almost certainly has to get rewritten, as l-kinds do
-   not support meets. *)
+    Pre-condition: the super jkind must be fully settled; no variables which
+    might be filled in later. Right now, if the super jkind has any
+    [with]-types, the sub jkind must have exactly the same [with]-types, in the
+    same order.
 
-(** Like [intersection_or_error], but between an [l] and an [l], as an [l]. *)
-val intersect_l_l :
-  reason:History.interact_reason ->
+    CR layouts v2.8: Implement this properly.
+*)
+val sub_jkind_l :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
   jkind_l ->
   jkind_l ->
   (jkind_l, Violation.t) result
 
+(** "round up" a [jkind_l] to a [jkind_r] such that the input is less than the
+    output. *)
+val round_up :
+  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
+  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  (allowed * 'r) t ->
+  ('l * allowed) t
+
+(** Map a function over types in [upper_bounds] *)
+val map_type_expr :
+  (Types.type_expr -> Types.type_expr) -> (allowed * 'r) t -> (allowed * 'r) t
+
 (** Checks to see whether a jkind is the maximum jkind. Never does any
     mutation. *)
 val is_max : ('l * allowed) t -> bool
@@ -559,9 +615,17 @@ val is_value_for_printing : 'd t -> bool
 (* debugging *)
 
 module Debug_printers : sig
-  val t : Format.formatter -> 'd t -> unit
+  val t :
+    print_type_expr:(Format.formatter -> Types.type_expr -> unit) ->
+    Format.formatter ->
+    'd t ->
+    unit
 
   module Const : sig
-    val t : Format.formatter -> 'd Const.t -> unit
+    val t :
+      print_type_expr:(Format.formatter -> Types.type_expr -> unit) ->
+      Format.formatter ->
+      'd Const.t ->
+      unit
   end
 end
diff --git a/typing/jkind_axis.ml b/typing/jkind_axis.ml
index b81e66ad8ba..4fc6fe01e48 100644
--- a/typing/jkind_axis.ml
+++ b/typing/jkind_axis.ml
@@ -12,37 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module type Axis_s = sig
-  type t
-
-  val max : t
-
-  val min : t
-
-  val equal : t -> t -> bool
-
-  val less_or_equal : t -> t -> Misc.Le_result.t
-
-  val le : t -> t -> bool
-
-  val meet : t -> t -> t
-
-  val join : t -> t -> t
-
-  val print : Format.formatter -> t -> unit
-end
-
-module Of_lattice (L : Mode_intf.Lattice) = struct
-  include L
-
-  let less_or_equal a b : Misc.Le_result.t =
-    match le a b, le b a with
-    | true, true -> Equal
-    | true, false -> Less
-    | false, _ -> Not_le
-
-  let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
-end
+module type Lattice = Mode_intf.Lattice
 
 module Externality = struct
   type t =
@@ -54,6 +24,8 @@ module Externality = struct
 
   let min = External
 
+  let legacy = Internal
+
   let equal e1 e2 =
     match e1, e2 with
     | External, External -> true
@@ -83,10 +55,10 @@ module Externality = struct
 
   let join t1 t2 =
     match t1, t2 with
-    | Internal, (External | External64 | Internal)
-    | (External | External64), Internal ->
+    | Internal, (Internal | External64 | External)
+    | (External64 | External), Internal ->
       Internal
-    | External64, (External | External64) | External, External64 -> External64
+    | External64, (External64 | External) | External, External64 -> External64
     | External, External -> External
 
   let print ppf = function
@@ -104,6 +76,8 @@ module Nullability = struct
 
   let min = Non_null
 
+  let legacy = Non_null
+
   let equal n1 n2 =
     match n1, n2 with
     | Non_null, Non_null -> true
@@ -126,7 +100,7 @@ module Nullability = struct
 
   let join n1 n2 =
     match n1, n2 with
-    | Maybe_null, (Non_null | Maybe_null) | Non_null, Maybe_null -> Maybe_null
+    | Maybe_null, (Maybe_null | Non_null) | Non_null, Maybe_null -> Maybe_null
     | Non_null, Non_null -> Non_null
 
   let print ppf = function
@@ -169,26 +143,26 @@ module Axis = struct
     let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
   end
 
-  let get (type a) : a t -> (module Axis_s with type t = a) = function
+  let get (type a) : a t -> (module Lattice with type t = a) = function
     | Modal Locality ->
-      (module Accent_lattice (Mode.Locality.Const) : Axis_s with type t = a)
+      (module Accent_lattice (Mode.Locality.Const) : Lattice with type t = a)
     | Modal Linearity ->
-      (module Accent_lattice (Mode.Linearity.Const) : Axis_s with type t = a)
+      (module Accent_lattice (Mode.Linearity.Const) : Lattice with type t = a)
     | Modal Uniqueness ->
-      (module Accent_lattice (Mode.Uniqueness.Const) : Axis_s with type t = a)
+      (module Accent_lattice (Mode.Uniqueness.Const) : Lattice with type t = a)
     | Modal Portability ->
-      (module Accent_lattice (Mode.Portability.Const) : Axis_s with type t = a)
+      (module Accent_lattice (Mode.Portability.Const) : Lattice with type t = a)
     | Modal Contention ->
-      (module Accent_lattice (Mode.Contention.Const) : Axis_s with type t = a)
-    | Nonmodal Externality -> (module Externality : Axis_s with type t = a)
-    | Nonmodal Nullability -> (module Nullability : Axis_s with type t = a)
+      (module Accent_lattice (Mode.Contention.Const) : Lattice with type t = a)
+    | Nonmodal Externality -> (module Externality : Lattice with type t = a)
+    | Nonmodal Nullability -> (module Nullability : Lattice with type t = a)
 
   let all =
     [ Pack (Modal Locality);
-      Pack (Modal Linearity);
       Pack (Modal Uniqueness);
-      Pack (Modal Portability);
+      Pack (Modal Linearity);
       Pack (Modal Contention);
+      Pack (Modal Portability);
       Pack (Nonmodal Externality);
       Pack (Nonmodal Nullability) ]
 
@@ -200,21 +174,34 @@ module Axis = struct
     | Modal Contention -> "contention"
     | Nonmodal Externality -> "externality"
     | Nonmodal Nullability -> "nullability"
+
+  let is_deep (type a) : a t -> bool = function
+    | Modal Locality -> true
+    | Modal Linearity -> true
+    | Modal Uniqueness -> true
+    | Modal Portability -> true
+    | Modal Contention -> true
+    | Nonmodal Externality -> true
+    | Nonmodal Nullability -> false
+end
+
+module type Axed = sig
+  type (+'type_expr, 'd, 'axis) t constraint 'd = 'l * 'r
 end
 
 (* Sadly this needs to be functorized since we don't have higher-kinded types *)
-module Axis_collection (T : Misc.T1) = struct
-  type t =
-    { locality : Mode.Locality.Const.t T.t;
-      linearity : Mode.Linearity.Const.t T.t;
-      uniqueness : Mode.Uniqueness.Const.t T.t;
-      portability : Mode.Portability.Const.t T.t;
-      contention : Mode.Contention.Const.t T.t;
-      externality : Externality.t T.t;
-      nullability : Nullability.t T.t
+module Axis_collection (T : Axed) = struct
+  type (+'type_expr, 'd) t =
+    { locality : ('type_expr, 'd, Mode.Locality.Const.t) T.t;
+      linearity : ('type_expr, 'd, Mode.Linearity.Const.t) T.t;
+      uniqueness : ('type_expr, 'd, Mode.Uniqueness.Const.t) T.t;
+      portability : ('type_expr, 'd, Mode.Portability.Const.t) T.t;
+      contention : ('type_expr, 'd, Mode.Contention.Const.t) T.t;
+      externality : ('type_expr, 'd, Externality.t) T.t;
+      nullability : ('type_expr, 'd, Nullability.t) T.t
     }
 
-  let get (type a) ~(axis : a Axis.t) values : a T.t =
+  let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t =
     match axis with
     | Modal Locality -> values.locality
     | Modal Linearity -> values.linearity
@@ -224,7 +211,7 @@ module Axis_collection (T : Misc.T1) = struct
     | Nonmodal Externality -> values.externality
     | Nonmodal Nullability -> values.nullability
 
-  let set (type a) ~(axis : a Axis.t) values (value : a T.t) =
+  let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) =
     match axis with
     | Modal Locality -> { values with locality = value }
     | Modal Linearity -> { values with linearity = value }
@@ -234,19 +221,152 @@ module Axis_collection (T : Misc.T1) = struct
     | Nonmodal Externality -> { values with externality = value }
     | Nonmodal Nullability -> { values with nullability = value }
 
-  (* Since we don't have polymorphic parameters, use a record to pass the polymorphic
-     function *)
-  module Create_f = struct
-    type t = { f : 'a. axis:'a Axis.t -> 'a T.t }
+  (* Since we don't have polymorphic parameters, use a record to pass the
+     polymorphic function *)
+  module Create = struct
+    module Monadic (M : Misc.Stdlib.Monad.S) = struct
+      type ('type_expr, 'd) f =
+        { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t M.t }
+      [@@unboxed]
+
+      let[@inline] f { f } =
+        let open M.Syntax in
+        let* locality = f ~axis:Axis.(Modal Locality) in
+        let* uniqueness = f ~axis:Axis.(Modal Uniqueness) in
+        let* linearity = f ~axis:Axis.(Modal Linearity) in
+        let* contention = f ~axis:Axis.(Modal Contention) in
+        let* portability = f ~axis:Axis.(Modal Portability) in
+        let* externality = f ~axis:Axis.(Nonmodal Externality) in
+        let* nullability = f ~axis:Axis.(Nonmodal Nullability) in
+        M.return
+          { locality;
+            uniqueness;
+            linearity;
+            contention;
+            portability;
+            externality;
+            nullability
+          }
+    end
+    [@@inline]
+
+    module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity)
+
+    type ('type_expr, 'd) f = ('type_expr, 'd) Monadic_identity.f
+
+    let[@inline] f f = Monadic_identity.f f
   end
 
-  let create ({ f } : Create_f.t) =
-    { locality = f ~axis:Axis.(Modal Locality);
-      linearity = f ~axis:Axis.(Modal Linearity);
-      uniqueness = f ~axis:Axis.(Modal Uniqueness);
-      portability = f ~axis:Axis.(Modal Portability);
-      contention = f ~axis:Axis.(Modal Contention);
-      externality = f ~axis:Axis.(Nonmodal Externality);
-      nullability = f ~axis:Axis.(Nonmodal Nullability)
-    }
+  module Map = struct
+    module Monadic (M : Misc.Stdlib.Monad.S) = struct
+      type ('type_expr, 'd1, 'd2) f =
+        { f :
+            'axis.
+            axis:'axis Axis.t ->
+            ('type_expr, 'd1, 'axis) T.t ->
+            ('type_expr, 'd2, 'axis) T.t M.t
+        }
+      [@@unboxed]
+
+      module Create = Create.Monadic (M)
+
+      let[@inline] f { f } bounds =
+        Create.f { f = (fun ~axis -> f ~axis (get ~axis bounds)) }
+    end
+    [@@inline]
+
+    module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity)
+
+    type ('type_expr, 'd1, 'd2) f = ('type_expr, 'd1, 'd2) Monadic_identity.f
+
+    let[@inline] f f bounds = Monadic_identity.f f bounds
+  end
+
+  module Map2 = struct
+    module Monadic (M : Misc.Stdlib.Monad.S) = struct
+      type ('type_expr, 'd1, 'd2, 'd3) f =
+        { f :
+            'axis.
+            axis:'axis Axis.t ->
+            ('type_expr, 'd1, 'axis) T.t ->
+            ('type_expr, 'd2, 'axis) T.t ->
+            ('type_expr, 'd3, 'axis) T.t M.t
+        }
+      [@@unboxed]
+
+      module Create = Create.Monadic (M)
+
+      let[@inline] f { f } bounds1 bounds2 =
+        Create.f
+          { f = (fun ~axis -> f ~axis (get ~axis bounds1) (get ~axis bounds2)) }
+    end
+    [@@inline]
+
+    module Monadic_identity = Monadic (Misc.Stdlib.Monad.Identity)
+
+    type ('type_expr, 'd1, 'd2, 'd3) f =
+      ('type_expr, 'd1, 'd2, 'd3) Monadic_identity.f
+
+    let[@inline] f f bounds1 bounds2 = Monadic_identity.f f bounds1 bounds2
+  end
+
+  module Fold = struct
+    type ('type_expr, 'd, 'r) f =
+      { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> 'r }
+    [@@unboxed]
+
+    let[@inline] f { f }
+        { locality;
+          linearity;
+          uniqueness;
+          portability;
+          contention;
+          externality;
+          nullability
+        } ~combine =
+      combine (f ~axis:Axis.(Modal Locality) locality)
+      @@ combine (f ~axis:Axis.(Modal Uniqueness) uniqueness)
+      @@ combine (f ~axis:Axis.(Modal Linearity) linearity)
+      @@ combine (f ~axis:Axis.(Modal Contention) contention)
+      @@ combine (f ~axis:Axis.(Modal Portability) portability)
+      @@ combine (f ~axis:Axis.(Nonmodal Externality) externality)
+      @@ f ~axis:Axis.(Nonmodal Nullability) nullability
+  end
+
+  module Fold2 = struct
+    type ('type_expr, 'd1, 'd2, 'r) f =
+      { f :
+          'axis.
+          axis:'axis Axis.t ->
+          ('type_expr, 'd1, 'axis) T.t ->
+          ('type_expr, 'd2, 'axis) T.t ->
+          'r
+      }
+    [@@unboxed]
+
+    let[@inline] f { f }
+        { locality = loc1;
+          linearity = lin1;
+          uniqueness = uni1;
+          portability = por1;
+          contention = con1;
+          externality = ext1;
+          nullability = nul1
+        }
+        { locality = loc2;
+          linearity = lin2;
+          uniqueness = uni2;
+          portability = por2;
+          contention = con2;
+          externality = ext2;
+          nullability = nul2
+        } ~combine =
+      combine (f ~axis:Axis.(Modal Locality) loc1 loc2)
+      @@ combine (f ~axis:Axis.(Modal Uniqueness) uni1 uni2)
+      @@ combine (f ~axis:Axis.(Modal Linearity) lin1 lin2)
+      @@ combine (f ~axis:Axis.(Modal Contention) con1 con2)
+      @@ combine (f ~axis:Axis.(Modal Portability) por1 por2)
+      @@ combine (f ~axis:Axis.(Nonmodal Externality) ext1 ext2)
+      @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2
+  end
 end
diff --git a/typing/jkind_axis.mli b/typing/jkind_axis.mli
index c3cf2aa42af..28bb37c2000 100644
--- a/typing/jkind_axis.mli
+++ b/typing/jkind_axis.mli
@@ -12,29 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** The common interface for jkind axes *)
-module type Axis_s = sig
-  type t
-
-  val max : t
-
-  val min : t
-
-  val equal : t -> t -> bool
-
-  val less_or_equal : t -> t -> Misc.Le_result.t
-
-  val le : t -> t -> bool
-
-  val meet : t -> t -> t
-
-  val join : t -> t -> t
-
-  val print : Format.formatter -> t -> unit
-end
-
-(** Adapt a [Lattice] to be an [Axis_s] *)
-module Of_lattice (L : Mode_intf.Lattice) : Axis_s with type t = L.t
+(** Re-export *)
+module type Lattice = Mode_intf.Lattice
 
 (** The jkind axis of Externality *)
 module Externality : sig
@@ -43,7 +22,7 @@ module Externality : sig
     | External64
     | Internal
 
-  include Axis_s with type t := t
+  include Lattice with type t := t
 end
 
 (** The jkind axis of nullability *)
@@ -52,7 +31,7 @@ module Nullability : sig
     | Non_null
     | Maybe_null
 
-  include Axis_s with type t := t
+  include Lattice with type t := t
 end
 
 module Axis : sig
@@ -82,35 +61,149 @@ module Axis : sig
   (* CR zqian: push ['a t] into the module to avoid first-class module. *)
 
   (** Given a jkind axis, get its interface *)
-  val get : 'a t -> (module Axis_s with type t = 'a)
+  val get : 'a t -> (module Lattice with type t = 'a)
 
   val all : packed list
 
   val name : _ t -> string
+
+  val is_deep : _ t -> bool
+end
+
+(** [Axed] describes a type that is parameterized by axis. *)
+module type Axed = sig
+  type (+'type_expr, 'd, 'axis) t constraint 'd = 'l * 'r
 end
 
 (** A collection with one item for each jkind axis.
-    [T] parametizes what element is being held for each axis. *)
-module Axis_collection (T : Misc.T1) : sig
-  type t =
-    { locality : Mode.Locality.Const.t T.t;
-      linearity : Mode.Linearity.Const.t T.t;
-      uniqueness : Mode.Uniqueness.Const.t T.t;
-      portability : Mode.Portability.Const.t T.t;
-      contention : Mode.Contention.Const.t T.t;
-      externality : Externality.t T.t;
-      nullability : Nullability.t T.t
+    [T] parametrizes what element is being held for each axis. *)
+module Axis_collection (T : Axed) : sig
+  (** [t] is parameterized over 'type_expr to enable usages in
+        [jkind_types.mli].  It is tempting to make those usages instead push the
+        [`type_expr] into the functor arg [T], but this leads to issues at
+        usages of [Jkind.t] in [types.mli] due to recursive definitions. *)
+  type (+'type_expr, 'd) t =
+    { locality : ('type_expr, 'd, Mode.Locality.Const.t) T.t;
+      linearity : ('type_expr, 'd, Mode.Linearity.Const.t) T.t;
+      uniqueness : ('type_expr, 'd, Mode.Uniqueness.Const.t) T.t;
+      portability : ('type_expr, 'd, Mode.Portability.Const.t) T.t;
+      contention : ('type_expr, 'd, Mode.Contention.Const.t) T.t;
+      externality : ('type_expr, 'd, Externality.t) T.t;
+      nullability : ('type_expr, 'd, Nullability.t) T.t
     }
 
-  val get : axis:'a Axis.t -> t -> 'a T.t
+  val get : axis:'a Axis.t -> ('type_expr, 'd) t -> ('type_expr, 'd, 'a) T.t
+
+  val set :
+    axis:'a Axis.t ->
+    ('type_expr, 'd) t ->
+    ('type_expr, 'd, 'a) T.t ->
+    ('type_expr, 'd) t
+
+  (** Create an axis collection by applying the function on each axis *)
+  module Create : sig
+    module Monadic (M : Misc.Stdlib.Monad.S) : sig
+      type ('type_expr, 'd) f =
+        { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t M.t }
+      [@@unboxed]
 
-  val set : axis:'a Axis.t -> t -> 'a T.t -> t
+      val f : ('type_expr, 'd) f -> ('type_expr, 'd) t M.t
+    end
 
-  module Create_f : sig
     (** This record type is used to pass a polymorphic function to [create] *)
-    type t = { f : 'a. axis:'a Axis.t -> 'a T.t }
+    type ('type_expr, 'd) f =
+      ('type_expr, 'd) Monadic(Misc.Stdlib.Monad.Identity).f
+
+    val f : ('type_expr, 'd) f -> ('type_expr, 'd) t
   end
 
-  (** Create an axis collection by applying the function on each axis *)
-  val create : Create_f.t -> t
+  (** Map an operation over all the bounds *)
+  module Map : sig
+    module Monadic (M : Misc.Stdlib.Monad.S) : sig
+      type ('type_expr, 'd1, 'd2) f =
+        { f :
+            'axis.
+            axis:'axis Axis.t ->
+            ('type_expr, 'd1, 'axis) T.t ->
+            ('type_expr, 'd2, 'axis) T.t M.t
+        }
+      [@@unboxed]
+
+      val f :
+        ('type_expr, 'd1, 'd2) f ->
+        ('type_expr, 'd1) t ->
+        ('type_expr, 'd2) t M.t
+    end
+
+    type ('type_expr, 'd1, 'd2) f =
+      ('type_expr, 'd1, 'd2) Monadic(Misc.Stdlib.Monad.Identity).f
+
+    val f :
+      ('type_expr, 'd1, 'd2) f -> ('type_expr, 'd1) t -> ('type_expr, 'd2) t
+  end
+
+  (** Map an operation over two sets of bounds *)
+  module Map2 : sig
+    module Monadic (M : Misc.Stdlib.Monad.S) : sig
+      type ('type_expr, 'd1, 'd2, 'd3) f =
+        { f :
+            'axis.
+            axis:'axis Axis.t ->
+            ('type_expr, 'd1, 'axis) T.t ->
+            ('type_expr, 'd2, 'axis) T.t ->
+            ('type_expr, 'd3, 'axis) T.t M.t
+        }
+      [@@unboxed]
+
+      val f :
+        ('type_expr, 'd1, 'd2, 'd3) f ->
+        ('type_expr, 'd1) t ->
+        ('type_expr, 'd2) t ->
+        ('type_expr, 'd3) t M.t
+    end
+
+    type ('type_expr, 'd1, 'd2, 'd3) f =
+      ('type_expr, 'd1, 'd2, 'd3) Monadic(Misc.Stdlib.Monad.Identity).f
+
+    val f :
+      ('type_expr, 'd1, 'd2, 'd3) f ->
+      ('type_expr, 'd1) t ->
+      ('type_expr, 'd2) t ->
+      ('type_expr, 'd3) t
+  end
+
+  (** Fold an operation over the bounds to a summary value *)
+  module Fold : sig
+    type ('type_expr, 'd, 'r) f =
+      { f : 'axis. axis:'axis Axis.t -> ('type_expr, 'd, 'axis) T.t -> 'r }
+    [@@unboxed]
+
+    (** [combine] should be associative. *)
+    val f :
+      ('type_expr, 'd, 'r) f ->
+      ('type_expr, 'd) t ->
+      combine:('r -> 'r -> 'r) ->
+      'r
+  end
+
+  (** Fold an operation over two sets of bounds to a summary value *)
+  module Fold2 : sig
+    type ('type_expr, 'd1, 'd2, 'r) f =
+      { f :
+          'axis.
+          axis:'axis Axis.t ->
+          ('type_expr, 'd1, 'axis) T.t ->
+          ('type_expr, 'd2, 'axis) T.t ->
+          'r
+      }
+    [@@unboxed]
+
+    (** [combine] should be associative. *)
+    val f :
+      ('type_expr, 'd1, 'd2, 'r) f ->
+      ('type_expr, 'd1) t ->
+      ('type_expr, 'd2) t ->
+      combine:('r -> 'r -> 'r) ->
+      'r
+  end
 end
diff --git a/typing/jkind_types.ml b/typing/jkind_types.ml
index 3e2de57df11..7dc25a57ffd 100644
--- a/typing/jkind_types.ml
+++ b/typing/jkind_types.ml
@@ -522,79 +522,251 @@ module Layout = struct
   end
 end
 
-module Modes = Jkind_axis.Of_lattice (Mode.Alloc.Const)
+module Baggage = struct
+  type (+'type_expr, 'd) t =
+    | No_baggage : ('type_expr, 'l * 'r) t
+    | Baggage :
+        'type_expr * 'type_expr list
+        -> ('type_expr, 'l * Allowance.disallowed) t
+
+  let as_list : type l r. (_, l * r) t -> _ = function
+    | No_baggage -> []
+    | Baggage (ty, tys) -> ty :: tys
+
+  let has_baggage : type l r. (_, l * r) t -> _ = function
+    | No_baggage -> false
+    | Baggage _ -> true
+
+  open Allowance
+
+  include Magic_allow_disallow (struct
+    type ('type_expr, _, 'd) sided = ('type_expr, 'd) t constraint 'd = 'l * 'r
+
+    let disallow_left :
+        type l r. ('type_expr, l * r) t -> ('type_expr, disallowed * r) t =
+      function
+      | No_baggage -> No_baggage
+      | Baggage _ as b -> b
+
+    let disallow_right :
+        type l r. ('type_expr, l * r) t -> ('type_expr, l * disallowed) t =
+      function
+      | No_baggage -> No_baggage
+      | Baggage _ as b -> b
+
+    let allow_left :
+        type l r. ('type_expr, allowed * r) t -> ('type_expr, l * r) t =
+      function
+      | No_baggage -> No_baggage
+      | Baggage _ as b -> b
+
+    let allow_right :
+        type l r. ('type_expr, l * allowed) t -> ('type_expr, l * r) t =
+      function
+      | No_baggage -> No_baggage
+  end)
+
+  let try_allow_l :
+      type l r. ('type_expr, l * r) t -> ('type_expr, allowed * r) t option =
+    function
+    | No_baggage -> Some No_baggage
+    | Baggage _ as b -> Some b
+
+  let try_allow_r :
+      type l r. ('type_expr, l * r) t -> ('type_expr, l * allowed) t option =
+    function
+    | No_baggage -> Some No_baggage
+    | Baggage _ -> None
+
+  let map_type_expr (type l r) f :
+      ('type_expr, l * r) t -> ('type_expr, l * r) t = function
+    | No_baggage -> No_baggage
+    | Baggage (ty, tys) -> Baggage (f ty, List.map f tys)
+
+  let debug_print (type l r) ~print_type_expr ppf : (_, l * r) t -> _ =
+    let open Format in
+    function
+    | No_baggage -> fprintf ppf "No_baggage"
+    | Baggage (ty, tys) ->
+      fprintf ppf "Baggage @[[%a]@]"
+        (pp_print_list
+           ~pp_sep:(fun ppf () -> fprintf ppf ";@ ")
+           print_type_expr)
+        (ty :: tys)
+end
 
-module Layout_and_axes = struct
-  open Jkind_axis
+module Bound = struct
+  open Allowance
 
-  type ('layout, +'d) t =
-    { layout : 'layout;
-      modes_upper_bounds : Mode.Alloc.Const.t;
-      externality_upper_bound : Externality.t;
-      nullability_upper_bound : Nullability.t
+  type (+'type_expr, 'd, 'a) t =
+    { modifier : 'a;
+      baggage : ('type_expr, 'd) Baggage.t
     }
     constraint 'd = 'l * 'r
 
-  let map f t = { t with layout = f t.layout }
+  include Magic_allow_disallow (struct
+    type ('type_expr, 'a, 'd) sided = ('type_expr, 'd, 'a) t
 
-  let map_option f t =
-    match f t.layout with None -> None | Some layout -> Some { t with layout }
+    let disallow_left t = { t with baggage = Baggage.disallow_left t.baggage }
 
-  let equal_after_all_inference_is_done eq_layout
-      { layout = lay1;
-        modes_upper_bounds = modes1;
-        externality_upper_bound = ext1;
-        nullability_upper_bound = null1
-      }
-      { layout = lay2;
-        modes_upper_bounds = modes2;
-        externality_upper_bound = ext2;
-        nullability_upper_bound = null2
-      } =
-    eq_layout lay1 lay2 && Modes.equal modes1 modes2
-    && Externality.equal ext1 ext2
-    && Nullability.equal null1 null2
+    let disallow_right t = { t with baggage = Baggage.disallow_right t.baggage }
+
+    let allow_left t = { t with baggage = Baggage.allow_left t.baggage }
+
+    let allow_right t = { t with baggage = Baggage.allow_right t.baggage }
+  end)
+
+  let try_allow_l { modifier; baggage } =
+    match Baggage.try_allow_l baggage with
+    | Some baggage -> Some { modifier; baggage }
+    | None -> None
+
+  let try_allow_r { modifier; baggage } =
+    match Baggage.try_allow_r baggage with
+    | Some baggage -> Some { modifier; baggage }
+    | None -> None
+
+  let map_type_expr f t = { t with baggage = Baggage.map_type_expr f t.baggage }
+
+  let equal :
+      _ -> (_, allowed * allowed, _) t -> (_, allowed * allowed, _) t -> bool =
+   fun eq_axis { modifier = m1; baggage = b1 } { modifier = m2; baggage = b2 } ->
+    match b1, b2 with No_baggage, No_baggage -> eq_axis m1 m2
+
+  let debug_print ~print_type_expr print_modifier ppf { modifier; baggage } =
+    Format.fprintf ppf "@[{ modifier = %a;@ baggage = %a }@]" print_modifier
+      modifier
+      (Baggage.debug_print ~print_type_expr)
+      baggage
+end
+
+module Bounds = struct
+  open Jkind_axis
+  include Axis_collection (Bound)
+
+  include Allowance.Magic_allow_disallow (struct
+    type ('type_expr, _, 'd) sided = ('type_expr, 'd) t
+
+    let disallow_left bounds =
+      Map.f { f = (fun ~axis:_ bound -> Bound.disallow_left bound) } bounds
 
-  (* Once we have more interesting mode stuff, this won't be trivial. *)
-  let try_allow_l ({ layout = _; _ } as t) = Some t
+    let disallow_right bounds =
+      Map.f { f = (fun ~axis:_ bound -> Bound.disallow_right bound) } bounds
 
-  (* Once we have more interesting mode stuff, this won't be trivial. *)
-  let try_allow_r ({ layout = _; _ } as t) = Some t
+    let allow_left bounds =
+      Map.f { f = (fun ~axis:_ bound -> Bound.allow_left bound) } bounds
 
-  let sub sub_layout
-      { layout = lay1;
-        modes_upper_bounds = modes1;
-        externality_upper_bound = ext1;
-        nullability_upper_bound = null1
+    let allow_right bounds =
+      Map.f { f = (fun ~axis:_ bound -> Bound.allow_right bound) } bounds
+  end)
+
+  let map_type_expr f t =
+    Map.f { f = (fun ~axis:_ bound -> Bound.map_type_expr f bound) } t
+
+  let equal bounds1 bounds2 =
+    Fold2.f
+      { f =
+          (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 ->
+            let (module Bound_ops) = Axis.get axis in
+            Bound.equal Bound_ops.equal bound1 bound2)
       }
-      { layout = lay2;
-        modes_upper_bounds = modes2;
-        externality_upper_bound = ext2;
-        nullability_upper_bound = null2
-      } =
-    Misc.Le_result.combine_list
-      [ sub_layout lay1 lay2;
-        Modes.less_or_equal modes1 modes2;
-        Externality.less_or_equal ext1 ext2;
-        Nullability.less_or_equal null1 null2 ]
-    [@@inline]
-
-  let format format_layout ppf
-      { layout;
-        modes_upper_bounds;
-        externality_upper_bound;
-        nullability_upper_bound
+      ~combine:( && ) bounds1 bounds2
+
+  let debug_print ~print_type_expr ppf
+      { locality;
+        linearity;
+        uniqueness;
+        portability;
+        contention;
+        externality;
+        nullability
       } =
+    let print_bound print_mod = Bound.debug_print ~print_type_expr print_mod in
     Format.fprintf ppf
-      "{ layout = %a;@ modes_upper_bounds = %a;@ externality_upper_bound = \
-       %a;@ nullability_upper_bound = %a }"
-      format_layout layout Mode.Alloc.Const.print modes_upper_bounds
-      Externality.print externality_upper_bound Nullability.print
-      nullability_upper_bound
+      "@[{ locality = %a;@ linearity = %a;@ uniqueness = %a;@ portability = \
+       %a;@ contention = %a;@ externality = %a;@ nullability = %a }@]"
+      (print_bound Mode.Locality.Const.print)
+      locality
+      (print_bound Mode.Linearity.Const.print)
+      linearity
+      (print_bound Mode.Uniqueness.Const.print)
+      uniqueness
+      (print_bound Mode.Portability.Const.print)
+      portability
+      (print_bound Mode.Contention.Const.print)
+      contention
+      (print_bound Externality.print)
+      externality
+      (print_bound Nullability.print)
+      nullability
+end
+
+module Layout_and_axes = struct
+  type ('type_expr, 'layout, 'd) t =
+    { layout : 'layout;
+      upper_bounds : ('type_expr, 'd) Bounds.t
+    }
+    constraint 'd = 'l * 'r
+
+  module Allow_disallow = Allowance.Magic_allow_disallow (struct
+    type ('type_expr, 'layout, 'd) sided = ('type_expr, 'layout, 'd) t
+
+    let disallow_left t =
+      { t with upper_bounds = Bounds.disallow_left t.upper_bounds }
+
+    let disallow_right t =
+      { t with upper_bounds = Bounds.disallow_right t.upper_bounds }
+
+    let allow_left t =
+      { t with upper_bounds = Bounds.allow_left t.upper_bounds }
+
+    let allow_right t =
+      { t with upper_bounds = Bounds.allow_right t.upper_bounds }
+  end)
+
+  include Allow_disallow
+
+  let map f t = { t with layout = f t.layout }
+
+  let map_option f t =
+    match f t.layout with None -> None | Some layout -> Some { t with layout }
+
+  let map_type_expr f t =
+    { t with upper_bounds = Bounds.map_type_expr f t.upper_bounds }
+
+  let equal eq_layout { layout = lay1; upper_bounds = bounds1 }
+      { layout = lay2; upper_bounds = bounds2 } =
+    eq_layout lay1 lay2 && Bounds.equal bounds1 bounds2
+
+  let try_allow_l { layout; upper_bounds } =
+    let module Bounds_map_option = Bounds.Map.Monadic (Misc.Stdlib.Monad.Option) in
+    match
+      Bounds_map_option.f
+        { f = (fun ~axis:_ bound -> Bound.try_allow_l bound) }
+        upper_bounds
+    with
+    | Some upper_bounds -> Some { layout; upper_bounds }
+    | None -> None
+
+  let try_allow_r { layout; upper_bounds } =
+    let module Bounds_map_option = Bounds.Map.Monadic (Misc.Stdlib.Monad.Option) in
+    match
+      Bounds_map_option.f
+        { f = (fun ~axis:_ bound -> Bound.try_allow_r bound) }
+        upper_bounds
+    with
+    | Some upper_bounds -> Some { layout; upper_bounds }
+    | None -> None
+
+  let debug_print ~print_type_expr format_layout ppf { layout; upper_bounds } =
+    Format.fprintf ppf "{ layout = %a;@ upper_bounds = %a }" format_layout
+      layout
+      (Bounds.debug_print ~print_type_expr)
+      upper_bounds
 end
 
 module Jkind_desc = struct
-  type ('type_expr, 'd) t = (Sort.t Layout.t, 'd) Layout_and_axes.t
+  type ('type_expr, 'd) t = ('type_expr, Sort.t Layout.t, 'd) Layout_and_axes.t
 
   type 'type_expr packed = Pack : ('type_expr, 'd) t -> 'type_expr packed
   [@@unboxed]
@@ -624,5 +796,5 @@ type ('type_expr, 'd) t =
   }
 
 module Const = struct
-  type ('type_expr, +'d) t = (Layout.Const.t, 'd) Layout_and_axes.t
+  type ('type_expr, 'd) t = ('type_expr, Layout.Const.t, 'd) Layout_and_axes.t
 end
diff --git a/typing/jkind_types.mli b/typing/jkind_types.mli
index 3ad140be16d..00346163e65 100644
--- a/typing/jkind_types.mli
+++ b/typing/jkind_types.mli
@@ -16,16 +16,16 @@
    types in this file) rather than using this file directly, unless you
    are in [Types] or [Primitive]. *)
 
-(* This module defines types used in the module Jkind. This is to avoid
-   a mutual dependencies between jkind.ml(i) and types.ml(i) and bewteen
-   jkind.ml(i) and primitive.ml(i). Polymorphic versions of types are defined
-   here, with type parameters that are meant to be filled by types defined in
-   types.ml(i). jkind.ml(i) redefines the types from this file types.ml
-   with the type variables instantiated. types.ml also redefines the types
-   from this file with the type variables instantiated, but only for internal
-   use. primitive.ml(i) uses the type [Jkind.const], and types.ml(i) depends on
-   prmitive.ml(i), so [Jkind.const] is defined here and primitive.ml(i) also
-   uses this module.
+(* This module defines types used in the module Jkind. This is to avoid a mutual
+   dependencies between jkind.ml(i) and types.ml(i) and bewteen jkind.ml(i) and
+   primitive.ml(i). Polymorphic versions of types are defined here, with type
+   parameters that are meant to be filled by types defined in
+   types.ml(i). jkind.ml(i) redefines the types from this file types.ml with the
+   type variables instantiated. types.ml also redefines the types from this file
+   with the type variables instantiated, but only for internal
+   use. primitive.ml(i) uses the type [Jkind.Const.t], and types.ml(i) depends
+   on primitive.ml(i), so [Jkind.Const.t] is defined here and primitive.ml(i)
+   also uses this module.
 
    Dependency chain without Jkind_types:
          _____________________
@@ -106,56 +106,103 @@ module Layout : sig
   end
 end
 
+module Baggage : sig
+  type (+'type_expr, 'd) t =
+    | No_baggage : ('type_expr, 'l * 'r) t
+    (* There must always be at least one type. *)
+    | Baggage :
+        'type_expr * 'type_expr list
+        -> ('type_expr, 'l * Allowance.disallowed) t
+
+  val as_list : ('type_expr, 'l * 'r) t -> 'type_expr list
+
+  val has_baggage : ('type_expr, 'l * 'r) t -> bool
+end
+
+module Bound : sig
+  open Allowance
+
+  type (+'type_expr, 'd, 'a) t =
+    { modifier : 'a;
+      baggage : ('type_expr, 'd) Baggage.t
+    }
+    constraint 'd = 'l * 'r
+
+  val try_allow_l :
+    ('type_expr, 'l * 'r, 'a) t -> ('type_expr, allowed * 'r, 'a) t option
+
+  val try_allow_r :
+    ('type_expr, 'l * 'r, 'a) t -> ('type_expr, 'l * allowed, 'a) t option
+end
+
+module Bounds : sig
+  include module type of Jkind_axis.Axis_collection (Bound)
+
+  include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) t
+
+  val debug_print :
+    print_type_expr:(Format.formatter -> 'type_expr -> unit) ->
+    Format.formatter ->
+    ('type_expr, 'd) t ->
+    unit
+end
+
 module Layout_and_axes : sig
   open Allowance
 
-  (* We need the variance annotation here to allow [any_dummy_jkind] to be
-     polymorphic in its allowances. Otherwise the value restriction bites.
-     Sigh. *)
-  type ('layout, +'d) t =
+  type (+'type_expr, 'layout, 'd) t =
     { layout : 'layout;
-      modes_upper_bounds : Mode.Alloc.Const.t;
-      externality_upper_bound : Jkind_axis.Externality.t;
-      nullability_upper_bound : Jkind_axis.Nullability.t
+      upper_bounds : ('type_expr, 'd) Bounds.t
     }
     constraint 'd = 'l * 'r
 
-  val map : ('a -> 'b) -> ('a, 'd) t -> ('b, 'd) t
+  module type Allow_disallow :=
+    Allow_disallow with type ('a, 'b, 'd) sided := ('a, 'b, 'd) t
+
+  module Allow_disallow : Allow_disallow
+
+  include Allow_disallow
+
+  val map : ('a -> 'b) -> ('type_expr, 'a, 'd) t -> ('type_expr, 'b, 'd) t
 
-  val map_option : ('a -> 'b option) -> ('a, 'd) t -> ('b, 'd) t option
+  val map_option :
+    ('a -> 'b option) -> ('type_expr, 'a, 'd) t -> ('type_expr, 'b, 'd) t option
 
-  (* An equality check should work over [lr]s only. But we need this
-     to do memoization in serialization. Happily, that's after all
-     inference is done, when worrying about l and r does not matter
-     any more. *)
-  val equal_after_all_inference_is_done :
-    ('layout -> 'layout -> bool) -> ('layout, 'd1) t -> ('layout, 'd2) t -> bool
+  val map_type_expr :
+    ('type_expr -> 'type_expr) ->
+    ('type_expr, 'a, 'd) t ->
+    ('type_expr, 'a, 'd) t
 
-  val try_allow_l : ('layout, 'l * 'r) t -> ('layout, allowed * 'r) t option
+  val equal :
+    ('layout -> 'layout -> bool) ->
+    ('type_expr, 'layout, allowed * allowed) t ->
+    ('type_expr, 'layout, allowed * allowed) t ->
+    bool
 
-  val try_allow_r : ('layout, 'l * 'r) t -> ('layout, 'l * allowed) t option
+  val try_allow_l :
+    ('type_expr, 'layout, 'l * 'r) t ->
+    ('type_expr, 'layout, allowed * 'r) t option
 
-  val sub :
-    ('layout -> 'layout -> Misc.Le_result.t) ->
-    ('layout, allowed * 'r) t ->
-    ('layout, 'l * allowed) t ->
-    Misc.Le_result.t
+  val try_allow_r :
+    ('type_expr, 'layout, 'l * 'r) t ->
+    ('type_expr, 'layout, 'l * allowed) t option
 
-  val format :
+  val debug_print :
+    print_type_expr:(Format.formatter -> 'type_expr -> unit) ->
     (Format.formatter -> 'layout -> unit) ->
     Format.formatter ->
-    ('layout, 'd) t ->
+    ('type_expr, 'layout, 'd) t ->
     unit
 end
 
 module Jkind_desc : sig
-  type ('type_expr, +'d) t = (Sort.t Layout.t, 'd) Layout_and_axes.t
+  type (+'type_expr, 'd) t = ('type_expr, Sort.t Layout.t, 'd) Layout_and_axes.t
 
-  type 'type_expr packed = Pack : ('type_expr, 'd) t -> 'type_expr packed
+  type +'type_expr packed = Pack : ('type_expr, 'd) t -> 'type_expr packed
   [@@unboxed]
 end
 
-type 'type_expr history =
+type +'type_expr history =
   | Interact of
       { reason : Jkind_intf.History.interact_reason;
         jkind1 : 'type_expr Jkind_desc.packed;
@@ -165,7 +212,7 @@ type 'type_expr history =
       }
   | Creation of Jkind_intf.History.creation_reason
 
-type ('type_expr, +'d) t =
+type (+'type_expr, 'd) t =
   { jkind : ('type_expr, 'd) Jkind_desc.t;
     annotation : Parsetree.jkind_annotation option;
     history : 'type_expr history;
@@ -174,5 +221,5 @@ type ('type_expr, +'d) t =
 
 (** CR layouts v2.8: remove this when printing is improved *)
 module Const : sig
-  type ('type_expr, +'d) t = (Layout.Const.t, 'd) Layout_and_axes.t
+  type (+'type_expr, 'd) t = ('type_expr, Layout.Const.t, 'd) Layout_and_axes.t
 end
diff --git a/typing/mode.ml b/typing/mode.ml
index e344ca4c173..9bbceee4f1b 100644
--- a/typing/mode.ml
+++ b/typing/mode.ml
@@ -25,6 +25,18 @@ type nonrec disallowed = disallowed
 
 type nonrec equate_step = equate_step
 
+module Make_lattice (L : Basic_lattice) = struct
+  include L
+
+  let less_or_equal a b : Misc.Le_result.t =
+    match le a b, le b a with
+    | true, true -> Equal
+    | true, false -> Less
+    | false, _ -> Not_le
+
+  let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
+end
+
 module type BiHeyting = sig
   (** Extend the [Lattice] interface with operations of bi-Heyting algebras *)
 
@@ -59,6 +71,10 @@ module Lattices = struct
 
     let print = L.print
 
+    let less_or_equal a b = L.less_or_equal b a
+
+    let equal = L.equal
+
     let imply a b = L.subtract b a
 
     let subtract a b = L.imply b a
@@ -67,8 +83,8 @@ module Lattices = struct
 
   (* A lattice is total order, if for any [a] [b], [a <= b] or [b <= a].
      A total lattice has a bi-heyting structure given as follows. *)
-  module Total (L : Lattice) : BiHeyting with type t := L.t = struct
-    include L
+  module Total (L : Basic_lattice) : BiHeyting with type t := L.t = struct
+    include Make_lattice (L)
 
     (* Prove the [subtract] below is the left adjoint of [join].
        - If [subtract a c <= b], by the definition of [subtract] below,
@@ -320,48 +336,56 @@ module Lattices = struct
   type monadic = Uniqueness.t * Contention.t
 
   module Monadic = struct
-    type t = monadic
+    include Make_lattice (struct
+      type t = monadic
+
+      let min = Uniqueness.min, Contention.min
 
-    let min = Uniqueness.min, Contention.min
+      let max = Uniqueness.max, Contention.max
 
-    let max = Uniqueness.max, Contention.max
+      let legacy = Uniqueness.legacy, Contention.legacy
 
-    let legacy = Uniqueness.legacy, Contention.legacy
+      let le (a0, a1) (b0, b1) = Uniqueness.le a0 b0 && Contention.le a1 b1
 
-    let le (a0, a1) (b0, b1) = Uniqueness.le a0 b0 && Contention.le a1 b1
+      let join (a0, a1) (b0, b1) = Uniqueness.join a0 b0, Contention.join a1 b1
 
-    let join (a0, a1) (b0, b1) = Uniqueness.join a0 b0, Contention.join a1 b1
+      let meet (a0, a1) (b0, b1) = Uniqueness.meet a0 b0, Contention.meet a1 b1
 
-    let meet (a0, a1) (b0, b1) = Uniqueness.meet a0 b0, Contention.meet a1 b1
+      let print ppf (a0, a1) =
+        Format.fprintf ppf "%a,%a" Uniqueness.print a0 Contention.print a1
+    end)
 
     let imply (a0, a1) (b0, b1) = Uniqueness.imply a0 b0, Contention.imply a1 b1
 
     let subtract (a0, a1) (b0, b1) =
       Uniqueness.subtract a0 b0, Contention.subtract a1 b1
-
-    let print ppf (a0, a1) =
-      Format.fprintf ppf "%a,%a" Uniqueness.print a0 Contention.print a1
   end
 
   type 'areality comonadic_with = 'areality * Linearity.t * Portability.t
 
   module Comonadic_with (Areality : Areality) = struct
-    type t = Areality.t comonadic_with
+    include Make_lattice (struct
+      type t = Areality.t comonadic_with
+
+      let min = Areality.min, Linearity.min, Portability.min
 
-    let min = Areality.min, Linearity.min, Portability.min
+      let max = Areality.max, Linearity.max, Portability.max
 
-    let max = Areality.max, Linearity.max, Portability.max
+      let legacy = Areality.legacy, Linearity.legacy, Portability.legacy
 
-    let legacy = Areality.legacy, Linearity.legacy, Portability.legacy
+      let le (a0, a1, a2) (b0, b1, b2) =
+        Areality.le a0 b0 && Linearity.le a1 b1 && Portability.le a2 b2
 
-    let le (a0, a1, a2) (b0, b1, b2) =
-      Areality.le a0 b0 && Linearity.le a1 b1 && Portability.le a2 b2
+      let join (a0, a1, a2) (b0, b1, b2) =
+        Areality.join a0 b0, Linearity.join a1 b1, Portability.join a2 b2
 
-    let join (a0, a1, a2) (b0, b1, b2) =
-      Areality.join a0 b0, Linearity.join a1 b1, Portability.join a2 b2
+      let meet (a0, a1, a2) (b0, b1, b2) =
+        Areality.meet a0 b0, Linearity.meet a1 b1, Portability.meet a2 b2
 
-    let meet (a0, a1, a2) (b0, b1, b2) =
-      Areality.meet a0 b0, Linearity.meet a1 b1, Portability.meet a2 b2
+      let print ppf (a0, a1, a2) =
+        Format.fprintf ppf "%a,%a,%a" Areality.print a0 Linearity.print a1
+          Portability.print a2
+    end)
 
     let imply (a0, a1, a2) (b0, b1, b2) =
       Areality.imply a0 b0, Linearity.imply a1 b1, Portability.imply a2 b2
@@ -370,10 +394,6 @@ module Lattices = struct
       ( Areality.subtract a0 b0,
         Linearity.subtract a1 b1,
         Portability.subtract a2 b2 )
-
-    let print ppf (a0, a1, a2) =
-      Format.fprintf ppf "%a,%a,%a" Areality.print a0 Linearity.print a1
-        Portability.print a2
   end
   [@@inline]
 
@@ -1745,46 +1765,50 @@ module Value_with (Areality : Areality) = struct
     { comonadic; monadic }
 
   module Const = struct
-    type t =
-      ( Areality.Const.t,
-        Linearity.Const.t,
-        Uniqueness.Const.t,
-        Portability.Const.t,
-        Contention.Const.t )
-      modes
-
     module Monadic = Monadic.Const
     module Comonadic = Comonadic.Const
 
-    let min = merge { comonadic = Comonadic.min; monadic = Monadic.min }
-
-    let max = merge { comonadic = Comonadic.max; monadic = Monadic.max }
-
-    let le m0 m1 =
-      let m0 = split m0 in
-      let m1 = split m1 in
-      Comonadic.le m0.comonadic m1.comonadic && Monadic.le m0.monadic m1.monadic
+    include Make_lattice (struct
+      type t =
+        ( Areality.Const.t,
+          Linearity.Const.t,
+          Uniqueness.Const.t,
+          Portability.Const.t,
+          Contention.Const.t )
+        modes
 
-    let print ppf m =
-      let { monadic; comonadic } = split m in
-      Format.fprintf ppf "%a,%a" Comonadic.print comonadic Monadic.print monadic
-
-    let legacy =
-      merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy }
-
-    let meet m0 m1 =
-      let m0 = split m0 in
-      let m1 = split m1 in
-      let monadic = Monadic.meet m0.monadic m1.monadic in
-      let comonadic = Comonadic.meet m0.comonadic m1.comonadic in
-      merge { monadic; comonadic }
-
-    let join m0 m1 =
-      let m0 = split m0 in
-      let m1 = split m1 in
-      let monadic = Monadic.join m0.monadic m1.monadic in
-      let comonadic = Comonadic.join m0.comonadic m1.comonadic in
-      merge { monadic; comonadic }
+      let min = merge { comonadic = Comonadic.min; monadic = Monadic.min }
+
+      let max = merge { comonadic = Comonadic.max; monadic = Monadic.max }
+
+      let le m0 m1 =
+        let m0 = split m0 in
+        let m1 = split m1 in
+        Comonadic.le m0.comonadic m1.comonadic
+        && Monadic.le m0.monadic m1.monadic
+
+      let print ppf m =
+        let { monadic; comonadic } = split m in
+        Format.fprintf ppf "%a,%a" Comonadic.print comonadic Monadic.print
+          monadic
+
+      let legacy =
+        merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy }
+
+      let meet m0 m1 =
+        let m0 = split m0 in
+        let m1 = split m1 in
+        let monadic = Monadic.meet m0.monadic m1.monadic in
+        let comonadic = Comonadic.meet m0.comonadic m1.comonadic in
+        merge { monadic; comonadic }
+
+      let join m0 m1 =
+        let m0 = split m0 in
+        let m1 = split m1 in
+        let monadic = Monadic.join m0.monadic m1.monadic in
+        let comonadic = Comonadic.join m0.comonadic m1.comonadic in
+        merge { monadic; comonadic }
+    end)
 
     module Option = struct
       type some = t
diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli
index cf30c298fb6..87a8f01aaaf 100644
--- a/typing/mode_intf.mli
+++ b/typing/mode_intf.mli
@@ -17,7 +17,7 @@ open Allowance
 (* While all our lattices are bi-Heyting algebras (see [mode.ml]), the extra
    structure is not directly useful to the user, so we only expose the basic
    lattice structure. *)
-module type Lattice = sig
+module type Basic_lattice = sig
   type t
 
   val min : t
@@ -35,6 +35,14 @@ module type Lattice = sig
   val print : Format.formatter -> t -> unit
 end
 
+module type Lattice = sig
+  include Basic_lattice
+
+  val less_or_equal : t -> t -> Misc.Le_result.t
+
+  val equal : t -> t -> bool
+end
+
 type equate_step =
   | Left_le_right
   | Right_le_left
diff --git a/typing/predef.ml b/typing/predef.ml
index 018e8c0a8a5..51ea61ae1d5 100644
--- a/typing/predef.ml
+++ b/typing/predef.ml
@@ -212,7 +212,12 @@ let option_argument_sort = Jkind.Sort.Const.value
 let option_argument_jkind = Jkind.Builtin.value ~why:(
   Type_argument {parent_path = path_option; position = 1; arity = 1})
 
-let list_jkind = Jkind.Builtin.value ~why:Boxed_variant
+(* CR layouts v2.8: Simplify this once we have a real subsumption check. *)
+let list_jkind param =
+  Jkind.add_baggage ~baggage:param
+    (Jkind.add_baggage ~baggage:(type_list param)
+       (Jkind.Builtin.immutable_data ~why:Boxed_variant))
+
 let list_sort = Jkind.Sort.Const.value
 let list_argument_sort = Jkind.Sort.Const.value
 let list_argument_jkind = Jkind.Builtin.value ~why:(
@@ -220,38 +225,41 @@ let list_argument_jkind = Jkind.Builtin.value ~why:(
 
 let or_null_argument_sort = Jkind.Sort.Const.value
 
-let mk_add_type add_type
+let mk_add_type add_type =
+  let add_type_with_jkind
       ?manifest type_ident
       ?(kind=Type_abstract Definition)
-      ?jkind
+      ~jkind
       env =
-  let type_jkind = match jkind with
-    | None -> Jkind.Builtin.value ~why:(Primitive type_ident)
-    | Some k -> Jkind.of_builtin ~why:(Primitive type_ident) k
+    let decl =
+      {type_params = [];
+       type_arity = 0;
+       type_kind = kind;
+       type_jkind = jkind;
+       type_loc = Location.none;
+       type_private = Asttypes.Public;
+       type_manifest = manifest;
+       type_variance = [];
+       type_separability = [];
+       type_is_newtype = false;
+       type_expansion_scope = lowest_level;
+       type_attributes = [];
+       type_unboxed_default = false;
+       type_uid = Uid.of_predef_id type_ident;
+       type_has_illegal_crossings = false;
+      }
+    in
+    add_type type_ident decl env
   in
-  let decl =
-    {type_params = [];
-     type_arity = 0;
-     type_kind = kind;
-     type_jkind;
-     type_loc = Location.none;
-     type_private = Asttypes.Public;
-     type_manifest = manifest;
-     type_variance = [];
-     type_separability = [];
-     type_is_newtype = false;
-     type_expansion_scope = lowest_level;
-     type_attributes = [];
-     type_unboxed_default = false;
-     type_uid = Uid.of_predef_id type_ident;
-     type_has_illegal_crossings = false;
-    }
+  let add_type ?manifest type_ident ?kind ~jkind env =
+    let jkind = Jkind.of_builtin ~why:(Primitive type_ident) jkind in
+    add_type_with_jkind ?manifest type_ident ?kind ~jkind env
   in
-  add_type type_ident decl env
+  add_type_with_jkind, add_type
 
 let mk_add_type1 add_type type_ident
       ?(kind=fun _ -> Type_abstract Definition)
-      ?(jkind=Jkind.Builtin.value ~why:(Primitive type_ident))
+      ~jkind
       ?(param_jkind=Jkind.Builtin.value ~why:(
         Type_argument {
           parent_path = Path.Pident type_ident;
@@ -264,7 +272,7 @@ let mk_add_type1 add_type type_ident
     {type_params = [param];
       type_arity = 1;
       type_kind = kind param;
-      type_jkind = jkind;
+      type_jkind = jkind param;
       type_loc = Location.none;
       type_private = Asttypes.Public;
       type_manifest = None;
@@ -337,7 +345,7 @@ let unrestricted tvar ca_sort =
 (* CR layouts: Changes will be needed here as we add support for the built-ins
    to work with non-values, and as we relax the mixed block restriction. *)
 let build_initial_env add_type add_extension empty_env =
-  let add_type = mk_add_type add_type
+  let add_type_with_jkind, add_type = mk_add_type add_type
   and add_type1 = mk_add_type1 add_type
   and add_extension = mk_add_extension add_extension in
   empty_env
@@ -347,17 +355,23 @@ let build_initial_env add_type add_extension empty_env =
        ~separability:Separability.Ind
        ~param_jkind:(Jkind.add_nullability_crossing
                       (Jkind.Builtin.any ~why:Array_type_argument))
+       ~jkind:(fun param ->
+         Jkind.add_baggage ~baggage:param
+           (Jkind.Builtin.mutable_data ~why:(Primitive ident_array)))
   |> add_type1 ident_iarray
        ~variance:Variance.covariant
        ~separability:Separability.Ind
        ~param_jkind:(Jkind.add_nullability_crossing
                       (Jkind.Builtin.any ~why:Array_type_argument))
+       ~jkind:(fun param ->
+         Jkind.add_baggage ~baggage:param
+           (Jkind.Builtin.immutable_data ~why:(Primitive ident_iarray)))
   |> add_type ident_bool
        ~kind:(variant [ cstr ident_false []; cstr ident_true []])
        ~jkind:Jkind.Const.Builtin.immediate
   |> add_type ident_char ~jkind:Jkind.Const.Builtin.immediate
   |> add_type ident_exn ~kind:Type_open ~jkind:Jkind.Const.Builtin.value
-  |> add_type ident_extension_constructor
+  |> add_type ident_extension_constructor ~jkind:Jkind.Const.Builtin.value
   |> add_type ident_float ~jkind:Jkind.Const.Builtin.immutable_data
   |> add_type ident_floatarray ~jkind:Jkind.Const.Builtin.mutable_data
   |> add_type ident_int ~jkind:Jkind.Const.Builtin.immediate
@@ -366,6 +380,8 @@ let build_initial_env add_type add_extension empty_env =
   |> add_type1 ident_lazy_t
        ~variance:Variance.covariant
        ~separability:Separability.Ind
+       (* CR layouts v2.8: Can [lazy_t] mode-cross at all? *)
+       ~jkind:(fun _ -> Jkind.Builtin.value ~why:(Primitive ident_lazy_t))
   |> add_type1 ident_list
        ~variance:Variance.covariant
        ~separability:Separability.Ind
@@ -382,8 +398,10 @@ let build_initial_env add_type add_extension empty_env =
        ~kind:(fun tvar ->
          variant [cstr ident_none [];
                   cstr ident_some [unrestricted tvar option_argument_sort]])
-       ~jkind:(Jkind.Builtin.value ~why:Boxed_variant)
-  |> add_type ident_lexing_position
+       ~jkind:(fun param ->
+         Jkind.add_baggage ~baggage:param
+           (Jkind.Builtin.immutable_data ~why:Boxed_variant))
+  |> add_type_with_jkind ident_lexing_position
        ~kind:(
          let lbl (field, field_type) =
            let id = Ident.create_predef field in
@@ -409,7 +427,15 @@ let build_initial_env add_type add_extension empty_env =
            (Record_boxed (List.map (fun label -> label.ld_sort) labels |> Array.of_list))
          )
        )
-       ~jkind:Jkind.Const.Builtin.immutable_data
+       (* CR layouts v2.8: Possibly remove this -- and simplify [mk_add_type] --
+          when we have a better jkind subsumption check. *)
+       ~jkind:Jkind.(
+         of_builtin Const.Builtin.immutable_data
+           ~why:(Primitive ident_lexing_position) |>
+         add_baggage ~baggage:type_int |>
+         add_baggage ~baggage:type_int |>
+         add_baggage ~baggage:type_int |>
+         add_baggage ~baggage:type_string)
   |> add_type ident_string ~jkind:Jkind.Const.Builtin.immutable_data
   |> add_type ident_unboxed_float ~jkind:Jkind.Const.Builtin.float64
   |> add_type ident_unboxed_nativeint ~jkind:Jkind.Const.Builtin.word
@@ -443,7 +469,7 @@ let build_initial_env add_type add_extension empty_env =
        Jkind.Sort.Const.value]
 
 let add_simd_stable_extension_types add_type env =
-  let add_type = mk_add_type add_type in
+  let _, add_type = mk_add_type add_type in
   env
   |> add_type ident_int8x16 ~jkind:Jkind.Const.Builtin.immutable_data
   |> add_type ident_int16x8 ~jkind:Jkind.Const.Builtin.immutable_data
@@ -459,7 +485,7 @@ let add_simd_stable_extension_types add_type env =
   |> add_type ident_unboxed_float64x2 ~jkind:Jkind.Const.Builtin.vec128
 
 let add_small_number_extension_types add_type env =
-  let add_type = mk_add_type add_type in
+  let _, add_type = mk_add_type add_type in
   env
   |> add_type ident_float32 ~jkind:Jkind.Const.Builtin.immutable_data
   |> add_type ident_unboxed_float32 ~jkind:Jkind.Const.Builtin.float32
@@ -481,8 +507,9 @@ let add_or_null add_type env =
      For now, we mark the type argument as [Separability.Ind] to permit
      the most argument types, and forbid arrays from accepting [or_null]s.
      In the future, we will track separability in the jkind system. *)
+  (* CR layouts v2.8: Add baggage and more mode crossing here. *)
   ~kind:or_null_kind
-  ~jkind:(Jkind.Builtin.value_or_null ~why:(Primitive ident_or_null))
+  ~jkind:(fun _ -> Jkind.Builtin.value_or_null ~why:(Primitive ident_or_null))
 
 let builtin_values =
   List.map (fun id -> (Ident.name id, id)) all_predef_exns
diff --git a/typing/predef.mli b/typing/predef.mli
index 71b1e05bc75..e9e9818c475 100644
--- a/typing/predef.mli
+++ b/typing/predef.mli
@@ -114,9 +114,9 @@ val ident_some : Ident.t
 val ident_or_null : Ident.t
 
 (* The jkind used for optional function argument types *)
-val option_argument_jkind : 'd jkind
+val option_argument_jkind : jkind_lr
 (* The jkind used for list argument types *)
-val list_argument_jkind : 'd jkind
+val list_argument_jkind : jkind_lr
 
 (* To build the initial environment. Since there is a nasty mutual
    recursion between predef and env, we break it by parameterizing
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index f75357288ad..3e8228407da 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -1690,7 +1690,9 @@ let type_expr ppf ty =
   prepare_for_printing [ty];
   prepared_type_expr ppf ty
 
-let () = Env.print_type_expr := type_expr
+let () =
+  Env.print_type_expr := type_expr;
+  Jkind.set_print_type_expr type_expr
 
 (* "Half-prepared" type expression: [ty] should have had its names reserved, but
    should not have had its loops marked. *)
diff --git a/typing/subst.ml b/typing/subst.ml
index d063669535e..9b779222398 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -84,7 +84,7 @@ let with_additional_action =
   (* Memoize the built-in jkinds *)
   let builtins =
     Jkind.Const.Builtin.all
-    |> List.map (fun (builtin : _ Jkind.Const.Builtin.t) ->
+    |> List.map (fun (builtin : Jkind.Const.Builtin.t) ->
           builtin.jkind,
           Jkind.of_const builtin.jkind
             ~annotation:(Some { pjkind_loc = Location.none;
@@ -111,7 +111,7 @@ let with_additional_action =
           | Some const ->
             let builtin =
               List.find_opt (fun (builtin, _) ->
-                  Jkind.Const.equal_after_all_inference_is_done const builtin)
+                  Jkind.Const.no_baggage_and_equal const builtin)
                 builtins
             in
             begin match builtin with
@@ -517,10 +517,13 @@ let type_declaration' copy_scope s decl =
       end;
     type_jkind =
       begin
-        match s.additional_action with
-        | Prepare_for_saving { prepare_jkind } ->
+        let jkind =
+          match s.additional_action with
+          | Prepare_for_saving { prepare_jkind } ->
             prepare_jkind decl.type_loc decl.type_jkind
-        | Duplicate_variables | No_action -> decl.type_jkind
+          | Duplicate_variables | No_action -> decl.type_jkind
+        in
+        Jkind.map_type_expr (typexp copy_scope s decl.type_loc) jkind
       end;
     type_private = decl.type_private;
     type_variance = decl.type_variance;
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 2e22cb486fe..95fe08d8a25 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -933,7 +933,11 @@ let mode_cross_left_value env ty mode =
   let mode =
     if not (is_principal ty) then mode else
     let jkind = type_jkind_purely env ty in
-    let upper_bounds = Jkind.get_modal_upper_bounds jkind in
+    let jkind_of_type = type_jkind_purely_if_principal env in
+    let type_equal = type_equal env in
+    let upper_bounds =
+      Jkind.get_modal_upper_bounds ~type_equal ~jkind_of_type jkind
+    in
     let upper_bounds = Const.alloc_as_value upper_bounds in
     Value.meet_const upper_bounds mode
   in
@@ -950,8 +954,12 @@ let alloc_mode_cross_to_max_min env ty { monadic; comonadic } =
   let monadic = Alloc.Monadic.disallow_left monadic in
   let comonadic = Alloc.Comonadic.disallow_right comonadic in
   if not (is_principal ty) then { monadic; comonadic } else
+  let type_equal = type_equal env in
   let jkind = type_jkind_purely env ty in
-  let upper_bounds = Jkind.get_modal_upper_bounds jkind in
+  let jkind_of_type = type_jkind_purely_if_principal env in
+  let upper_bounds =
+    Jkind.get_modal_upper_bounds ~type_equal ~jkind_of_type jkind
+  in
   let upper_bounds = Alloc.Const.split upper_bounds in
   let comonadic = Alloc.Comonadic.meet_const upper_bounds.comonadic comonadic in
   let monadic = Alloc.Monadic.imply upper_bounds.monadic monadic in
@@ -960,18 +968,22 @@ let alloc_mode_cross_to_max_min env ty { monadic; comonadic } =
 (** Mode cross a right mode *)
 (* This is very similar to Ctype.mode_cross_right. Any bugs here are likely bugs
    there, too. *)
-let expect_mode_cross_jkind jkind (expected_mode : expected_mode) =
-  let upper_bounds = Jkind.get_modal_upper_bounds jkind in
+let expect_mode_cross_jkind env jkind (expected_mode : expected_mode) =
+  let type_equal = type_equal env in
+  let jkind_of_type = type_jkind_purely_if_principal env in
+  let upper_bounds =
+    Jkind.get_modal_upper_bounds ~type_equal ~jkind_of_type jkind
+  in
   let upper_bounds = Const.alloc_as_value upper_bounds in
   mode_morph (Value.imply upper_bounds) expected_mode
 
 let expect_mode_cross env ty (expected_mode : expected_mode) =
   if not (is_principal ty) then expected_mode else
   let jkind = type_jkind_purely env ty in
-  expect_mode_cross_jkind jkind expected_mode
+  expect_mode_cross_jkind env jkind expected_mode
 
 (** The expected mode for objects *)
-let mode_object = expect_mode_cross_jkind Jkind.for_object mode_legacy
+let mode_object = expect_mode_cross_jkind Env.empty Jkind.for_object mode_legacy
 
 let mode_annots_from_pat pat =
   let modes =
@@ -9105,7 +9117,7 @@ and type_let ?check ?check_strict ?(force_toplevel = false)
       List.iter
         (fun pv ->
           Ctype.check_and_update_generalized_ty_jkind
-            ~name:pv.pv_id ~loc:pv.pv_loc pv.pv_type)
+            ~name:pv.pv_id ~loc:pv.pv_loc env pv.pv_type)
         pvs;
       List.iter2
         (fun (_, _, expected_ty) (exp, vars) ->
@@ -9134,7 +9146,7 @@ and type_let ?check ?check_strict ?(force_toplevel = false)
           | Tpat_alias(_, id, _, _, _) -> Some id
           | _ -> None in
         Ctype.check_and_update_generalized_ty_jkind
-          ?name:pat_name ~loc:exp.exp_loc exp.exp_type
+          ?name:pat_name ~loc:exp.exp_loc env exp.exp_type
       in
       List.iter2 update_exp_jkind mode_pat_typ_list exp_list;
     end
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index e68512ee2b5..6b156e070b0 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -145,6 +145,7 @@ type error =
       ; expected: Path.t
       }
   | Non_abstract_reexport of Path.t
+  | Illegal_baggage of jkind_l
 
 open Typedtree
 
@@ -266,7 +267,21 @@ let enter_type ?abstract_abbrevs rec_flag env sdecl (id, uid) =
   let type_jkind =
     Jkind.of_type_decl_default
       ~context:(Type_declaration path)
-      ~default:any
+      (* CR layouts v2.8: This next line is truly terrible. But I think it's OK
+         for now: it will mean that any [with] constraints get interpreted to
+         mean that the thing does not cross that mode. That's OK: the jkind
+         produced here can be an overapproximation of the correct jkind (note
+         that [any] is the default).  Indeed the only reason (I think) we need a
+         non-[any] jkind here is to produce better error messages.
+
+         Doing better here will be annoying, because a type is in scope in its
+         own jkind... and yet we don't have an env that we can use at this
+         point. I think probably the solution will be to have
+         [Jkind.of_type_decl_default] just return [max] every time it sees a
+         [with]-kind... which basically just does this [type_exn] trick but much
+         more sanely. *)
+      ~transl_type:(fun _ -> Predef.type_exn)
+      ~default:(Jkind.disallow_right any)
       sdecl
   in
   let abstract_source, type_manifest =
@@ -784,8 +799,28 @@ let transl_declaration env sdecl (id, uid) =
     | _ -> false, false (* Not unboxable, mark as boxed *)
   in
   verify_unboxed_attr unboxed_attr sdecl;
+  (* CR layouts v2.8: This next call to [transl_simple_type] probably can loop
+     because it will do perhaps-circular jkind checks. But actually I think the
+     same problem exists in e.g. record fields. We should probably look into this. *)
+  let transl_type sty =
+    (* CR layouts v2.8: The [~new_var_jkind:Any] is weird. The type is closed,
+       and so there shouldn't be any new vars. Investigate. *)
+    let cty =
+      Ctype.with_local_level begin fun () ->
+        Typetexp.transl_simple_type env ~new_var_jkind:Any
+          ~closed:true Mode.Alloc.Const.legacy sty
+      end
+      (* This call to [generalize_structure] is necessary so that copying
+         during instantiation traverses inside of any type constructors in the
+         [with]-bound. It's also necessary because the variables here are at
+         generic level, and so any containers of them should be, too! *)
+      ~post:(fun cty -> Ctype.generalize_structure cty.ctyp_type)
+    in
+    cty.ctyp_type  (* CR layouts v2.8: Do this more efficiently. Or probably
+                      add with-kinds to Typedtree. *)
+  in
   let jkind_from_annotation, jkind_annotation =
-    match Jkind.of_type_decl ~context:(Type_declaration path) sdecl with
+    match Jkind.of_type_decl ~context:(Type_declaration path) ~transl_type sdecl with
     | Some (jkind, annot) ->
         Some jkind, annot
     | None -> None, None
@@ -1179,12 +1214,36 @@ let narrow_to_manifest_jkind env loc decl =
   match decl.type_manifest with
   | None -> decl
   | Some ty ->
-    match
-      Ctype.constrain_type_jkind env ty (Jkind.terrible_relax_l decl.type_jkind)
-    with
-    | Ok () -> { decl with type_jkind = Ctype.estimate_type_jkind env ty }
-    | Error v ->
-      raise (Error (loc, Jkind_mismatch_of_type (ty,v)))
+    (* CR layouts v2.8: Remove this horrible hack. In practice, this
+       [try_allow_r] fails in the case of a record re-export, because the jkind
+       from the record has been calculated and put in decl.type_jkind at this
+       point.  So we need to use the deeply broken [type_jkind_purely] and then
+       [sub_jkind_l] here. The right way forward is to parameterize
+       [constrain_type_jkind] over the [l]-ness of its bound. But probably not
+       until we have proper subsumption working, as this hack will likely hold
+       up for a little while. *)
+    begin match Jkind.try_allow_r decl.type_jkind with
+    | None -> begin
+        let type_equal = Ctype.type_equal env in
+        let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in
+        let manifest_jkind = Ctype.type_jkind_purely env ty in
+        match
+          Jkind.sub_jkind_l ~type_equal ~jkind_of_type
+            manifest_jkind decl.type_jkind
+        with
+        | Ok _ -> ()
+        | Error v -> raise (Error (loc, Jkind_mismatch_of_type (ty,v)))
+      end
+    | Some type_jkind -> begin
+        match Ctype.constrain_type_jkind env ty type_jkind with
+        | Ok () -> ()
+        | Error v -> raise (Error (loc, Jkind_mismatch_of_type (ty,v)))
+      end
+    end;
+    (* Just use [estimate_type_jkind], as [type_jkind] does effectful
+       expansion (bad) and [type_jkind_purely] is broken; see comments
+       on that function. *)
+    { decl with type_jkind = Ctype.estimate_type_jkind env ty }
 
 (* Check that the type expression (if present) is compatible with the kind.
    If both a variant/record definition and a type equation are given,
@@ -1197,7 +1256,11 @@ let check_kind_coherence env loc dpath decl =
     Some ty ->
       if !Clflags.allow_illegal_crossing then begin
         let jkind' = Ctype.type_jkind_purely env ty in
-        begin match Jkind.sub_jkind_l jkind' decl.type_jkind with
+        let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in
+        let type_equal = Ctype.type_equal env in
+        begin match Jkind.sub_jkind_l
+                      ~type_equal ~jkind_of_type jkind' decl.type_jkind
+        with
         | Ok _ -> ()
         | Error v ->
           raise (Error (loc, Jkind_mismatch_of_type (ty,v)))
@@ -1247,6 +1310,7 @@ let check_abbrev env sdecl (id, decl) =
 *)
 (* [update_label_sorts] additionally returns whether all the jkinds
    were void, and the jkinds of the labels *)
+(* CR reisenberg: remove all_void return *)
 let update_label_sorts env loc lbls named =
   (* [named] is [Some sorts] for top-level records (we will update the
      sorts) and [None] for inlined records. *)
@@ -1357,7 +1421,11 @@ module Element_repr = struct
     else
       let layout = Jkind.get_layout_defaulting_to_value jkind in
       let sort = Jkind.Layout.Const.get_sort layout in
-      let externality_upper_bound = Jkind.get_externality_upper_bound jkind in
+      let type_equal = Ctype.type_equal env in
+      let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in
+      let externality_upper_bound =
+        Jkind.get_externality_upper_bound ~type_equal ~jkind_of_type jkind
+      in
       let base = match sort with
         | None ->
             Misc.fatal_error "Element_repr.classify: unexpected abstract layout"
@@ -1544,10 +1612,10 @@ let update_decl_jkind env dpath decl =
       let ld_sort = Jkind.Sort.default_to_value_and_get sort in
       [{lbl with ld_sort}], Record_unboxed, jkind
     | _, Record_boxed sorts ->
-      let lbls, all_void, jkinds =
+      let lbls, _all_void, jkinds =
         update_label_sorts env loc lbls (Some sorts)
       in
-      let jkind = Jkind.for_boxed_record ~all_void in
+      let jkind = Jkind.for_boxed_record lbls in
       let reprs =
         List.map2
           (fun lbl jkind ->
@@ -1673,8 +1741,8 @@ let update_decl_jkind env dpath decl =
           assert false
       end
     | cstrs, Variant_boxed cstr_shapes ->
-      let (_,cstrs,all_voids) =
-        List.fold_left (fun (idx,cstrs,all_voids) cstr ->
+      let (_,cstrs) =
+        List.fold_left (fun (idx,cstrs) cstr ->
           let arg_sorts =
             match cstr_shapes.(idx) with
             | Constructor_uniform_value, arg_sorts -> arg_sorts
@@ -1683,7 +1751,7 @@ let update_decl_jkind env dpath decl =
                   "Typedecl.update_variant_kind doesn't expect mixed \
                    constructor as input"
           in
-          let cd_args, all_void, jkinds =
+          let cd_args, _all_void, jkinds =
             update_constructor_arguments_sorts env cstr.Types.cd_loc
               cstr.Types.cd_args (Some arg_sorts)
           in
@@ -1698,18 +1766,22 @@ let update_decl_jkind env dpath decl =
             | Constructor_mixed _ -> cstr_shapes.(idx) <- cstr_repr, arg_sorts
           in
           let cstr = { cstr with Types.cd_args } in
-          (idx+1,cstr::cstrs,all_voids && all_void)
-        ) (0,[],true) cstrs
+          (idx+1,cstr::cstrs)
+        ) (0,[]) cstrs
       in
-      let jkind = Jkind.for_boxed_variant ~all_voids in
+      let jkind = Jkind.for_boxed_variant cstrs in
       List.rev cstrs, rep, jkind
     | (([] | (_ :: _)), Variant_unboxed | _, Variant_extensible) ->
       assert false
   in
 
+  let type_equal = Ctype.type_equal env in
+  let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in
+
   let add_crossings jkind =
     match !Clflags.allow_illegal_crossing with
-    | true -> Jkind.add_portability_and_contention_crossing ~from:decl.type_jkind jkind
+    | true -> Jkind.add_portability_and_contention_crossing
+                ~type_equal ~jkind_of_type ~from:decl.type_jkind jkind
     | false -> jkind, false
   in
 
@@ -1767,22 +1839,27 @@ let update_decl_jkind env dpath decl =
 
   (* check that the jkind computed from the kind matches the jkind
      annotation, which was stored in decl.type_jkind *)
-  if new_jkind != decl.type_jkind then
+  if new_jkind != decl.type_jkind then begin
     (* CR layouts v2.8: Consider making a function that doesn't compute
        histories for this use-case, which doesn't need it. *)
-    begin match Jkind.sub_jkind_l new_jkind decl.type_jkind with
+    (* The [decl.type_jkind] should never have [with]-types in it at this
+       point. *)
+    let type_equal _ _ = false in
+    match Jkind.sub_jkind_l ~type_equal ~jkind_of_type
+            new_jkind decl.type_jkind
+    with
     | Ok _ -> ()
     | Error err ->
       raise(Error(decl.type_loc, Jkind_mismatch_of_path (dpath,err)))
     end;
   new_decl
 
-let update_decls_jkind_reason decls =
+let update_decls_jkind_reason env decls =
   List.map
     (fun (id, decl) ->
        let update_generalized =
         Ctype.check_and_update_generalized_ty_jkind
-          ~name:id ~loc:decl.type_loc
+          ~name:id ~loc:decl.type_loc env
        in
        List.iter update_generalized decl.type_params;
        Btype.iter_type_expr_kind update_generalized decl.type_kind;
@@ -2393,7 +2470,7 @@ let transl_type_decl env rec_flag sdecl_list =
       |> Typedecl_variance.update_decls env sdecl_list
       |> Typedecl_separability.update_decls env
       |> update_decls_jkind new_env
-      |> update_decls_jkind_reason
+      |> update_decls_jkind_reason new_env
     with
     | Typedecl_variance.Error (loc, err) ->
         raise (Error (loc, Variance err))
@@ -3168,7 +3245,7 @@ let transl_value_decl env loc ~sig_modalities valdecl =
     Env.enter_value ~mode:Mode.Value.legacy valdecl.pval_name.txt v env
       ~check:(fun s -> Warnings.Unused_value_declaration s)
   in
-  Ctype.check_and_update_generalized_ty_jkind ~name:id ~loc ty;
+  Ctype.check_and_update_generalized_ty_jkind ~name:id ~loc newenv ty;
   let desc =
     {
      val_id = id;
@@ -3400,9 +3477,17 @@ let approx_type_decl sdecl_list =
        let id = Ident.create_scoped ~scope sdecl.ptype_name.txt in
        let path = Path.Pident id in
        let injective = sdecl.ptype_kind <> Ptype_abstract in
+       let transl_type sty =
+         Misc.fatal_errorf
+           "@[I do not yet know how to deal with [with]-types (such as %a)@ in \
+            recursive modules. Please contact the Jane Street OCaml Language@ \
+            team for help if you see this."
+           Pprintast.core_type sty
+       in
        let jkind =
          Jkind.of_type_decl_default
            ~context:(Type_declaration path)
+           ~transl_type
            ~default:(Jkind.Builtin.value ~why:Default_type_jkind)
            sdecl
        in
@@ -3977,6 +4062,10 @@ let report_error ppf = function
       "@[Invalid reexport declaration.\
          @ Type %s must not define an explicit representation.@]"
       (Path.name definition)
+  | Illegal_baggage jkind ->
+    fprintf ppf
+      "@[Illegal %a in kind annotation of an abbreviation:@ %a@]"
+      Style.inline_code "with" Jkind.format jkind
 
 let () =
   Location.register_error_of_exn
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index 13693ebd5a7..523ef10e85f 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -181,6 +181,7 @@ type error =
       ; expected: Path.t
       }
   | Non_abstract_reexport of Path.t
+  | Illegal_baggage of jkind_l
 
 exception Error of Location.t * error
 
diff --git a/typing/typedecl_separability.ml b/typing/typedecl_separability.ml
index 829a4573cc6..7a7946f5702 100644
--- a/typing/typedecl_separability.ml
+++ b/typing/typedecl_separability.ml
@@ -482,8 +482,13 @@ let msig_of_external_type env decl =
     Result.is_error (Ctype.check_decl_jkind env decl
                         (Jkind.Builtin.value_or_null ~why:Separability_check))
   in
+  let type_equal = Ctype.type_equal env in
+  let jkind_of_type = Ctype.type_jkind_purely_if_principal env in
   let is_external =
-    match Jkind.get_externality_upper_bound decl.type_jkind with
+    match
+      Jkind.get_externality_upper_bound ~type_equal ~jkind_of_type
+        decl.type_jkind
+    with
     | Internal -> false
     | External | External64 -> true
   in
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 91001694222..c0fdf1de42f 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -754,6 +754,7 @@ let merge_constraint initial_env loc sg lid constr =
            check is repeated later -- and with better handling for errors -- we
            just drop any error here. *)
         ignore
+          (* CR layouts v2.8: Does this type_jkind need to be instantiated? *)
           (Ctype.constrain_decl_jkind initial_env tdecl sig_decl.type_jkind);
         check_type_decl outer_sig_env sg_for_env loc id None tdecl sig_decl;
         let tdecl = { tdecl with type_manifest = None } in
diff --git a/typing/typemode.ml b/typing/typemode.ml
index 8cbd18650c7..b14e9ca99b9 100644
--- a/typing/typemode.ml
+++ b/typing/typemode.ml
@@ -55,29 +55,39 @@ module Axis_pair = struct
 end
 
 let transl_annot (type m) ~(annot_type : m annot_type) ~required_mode_maturity
-    annot : m Axis_pair.t =
+    annot : m Axis_pair.t Location.loc =
   Option.iter
     (fun maturity ->
       Language_extension.assert_enabled ~loc:annot.loc Mode maturity)
     required_mode_maturity;
-  match Axis_pair.of_string annot.txt, annot_type with
-  | Any_axis_pair (Nonmodal _, _), (Mode | Modality) | (exception Not_found) ->
-    raise (Error (annot.loc, Unrecognized_modifier (annot_type, annot.txt)))
-  | Any_axis_pair (Modal axis, mode), Mode -> Modal_axis_pair (axis, mode)
-  | Any_axis_pair (Modal axis, mode), Modality -> Modal_axis_pair (axis, mode)
-  | pair, Modifier -> pair
+  let pair : m Axis_pair.t =
+    match Axis_pair.of_string annot.txt, annot_type with
+    | Any_axis_pair (Nonmodal _, _), (Mode | Modality) | (exception Not_found)
+      ->
+      raise (Error (annot.loc, Unrecognized_modifier (annot_type, annot.txt)))
+    | Any_axis_pair (Modal axis, mode), Mode -> Modal_axis_pair (axis, mode)
+    | Any_axis_pair (Modal axis, mode), Modality -> Modal_axis_pair (axis, mode)
+    | pair, Modifier -> pair
+  in
+  { txt = pair; loc = annot.loc }
 
 let unpack_mode_annot { txt = Parsetree.Mode s; loc } = { txt = s; loc }
 
-module Opt_axis_collection = Axis_collection (Option)
+module Transled_modifier = struct
+  type (_, 'd, 'a) t = 'a Location.loc option constraint 'd = 'l * 'r
+
+  let drop_loc modifier = Option.map Location.get_txt modifier
+end
+
+module Transled_modifiers = Jkind_axis.Axis_collection (Transled_modifier)
 
 let transl_modifier_annots annots =
   let step modifiers_so_far annot =
-    let (Any_axis_pair (type a) ((axis, mode) : a Axis.t * a)) =
+    let { txt = Any_axis_pair (type a) ((axis, mode) : a Axis.t * a); loc } =
       transl_annot ~annot_type:Modifier ~required_mode_maturity:None
       @@ unpack_mode_annot annot
     in
-    let (module A : Axis_s with type t = a) = Axis.get axis in
+    let (module A : Mode_intf.Lattice with type t = a) = Axis.get axis in
     let is_top = A.le A.max mode in
     if is_top
     then
@@ -87,36 +97,38 @@ let transl_modifier_annots annots =
       (* Location.prerr_warning new_raw.loc (Warnings.Mod_by_top new_raw.txt) *)
       ();
     let is_dup =
-      Option.is_some (Opt_axis_collection.get ~axis modifiers_so_far)
+      Option.is_some (Transled_modifiers.get ~axis modifiers_so_far)
     in
     if is_dup then raise (Error (annot.loc, Duplicated_axis axis));
-    Opt_axis_collection.set ~axis modifiers_so_far (Some mode)
+    Transled_modifiers.set ~axis modifiers_so_far (Some { txt = mode; loc })
   in
   let empty_modifiers =
-    Opt_axis_collection.create { f = (fun ~axis:_ -> None) }
+    Transled_modifiers.Create.f { f = (fun ~axis:_ -> None) }
   in
   List.fold_left step empty_modifiers annots
 
 let transl_mode_annots annots : Alloc.Const.Option.t =
   let step modifiers_so_far annot =
-    let (Modal_axis_pair (type a) ((axis, mode) : a Axis.Modal.t * a)) =
+    let { txt = Modal_axis_pair (type a) ((axis, mode) : a Axis.Modal.t * a);
+          loc
+        } =
       transl_annot ~annot_type:Mode ~required_mode_maturity:(Some Stable)
       @@ unpack_mode_annot annot
     in
     let axis = Axis.Modal axis in
-    if Option.is_some (Opt_axis_collection.get ~axis modifiers_so_far)
+    if Option.is_some (Transled_modifiers.get ~axis modifiers_so_far)
     then raise (Error (annot.loc, Duplicated_axis axis));
-    Opt_axis_collection.set ~axis modifiers_so_far (Some mode)
+    Transled_modifiers.set ~axis modifiers_so_far (Some { txt = mode; loc })
   in
   let empty_modifiers =
-    Opt_axis_collection.create { f = (fun ~axis:_ -> None) }
+    Transled_modifiers.Create.f { f = (fun ~axis:_ -> None) }
   in
   let modes = List.fold_left step empty_modifiers annots in
-  { areality = modes.locality;
-    linearity = modes.linearity;
-    uniqueness = modes.uniqueness;
-    portability = modes.portability;
-    contention = modes.contention
+  { areality = Transled_modifier.drop_loc modes.locality;
+    linearity = Transled_modifier.drop_loc modes.linearity;
+    uniqueness = Transled_modifier.drop_loc modes.uniqueness;
+    portability = Transled_modifier.drop_loc modes.portability;
+    contention = Transled_modifier.drop_loc modes.contention
   }
 
 let untransl_mode_annots ~loc (modes : Mode.Alloc.Const.Option.t) =
@@ -143,7 +155,7 @@ let transl_modality ~maturity { txt = Parsetree.Modality modality; loc } =
     transl_annot ~annot_type:Modality ~required_mode_maturity:(Some maturity)
       { txt = modality; loc }
   in
-  match axis_pair with
+  match axis_pair.txt with
   | Modal_axis_pair (Locality, mode) ->
     Modality.Atom
       (Comonadic Areality, Meet_with (Const.locality_as_regionality mode))
diff --git a/typing/typemode.mli b/typing/typemode.mli
index 96fdd145b68..1d74dfbf496 100644
--- a/typing/typemode.mli
+++ b/typing/typemode.mli
@@ -30,7 +30,13 @@ val untransl_modalities :
   Mode.Modality.Value.Const.t ->
   Parsetree.modalities
 
+module Transled_modifier : sig
+  type (_, 'd, 'a) t = 'a Location.loc option constraint 'd = 'l * 'r
+end
+
+module Transled_modifiers :
+    module type of Jkind_axis.Axis_collection (Transled_modifier)
+
 (** Interpret a list of modifiers.
     A "modifier" is any keyword coming after a `mod` in a jkind *)
-val transl_modifier_annots :
-  Parsetree.modes -> Jkind_axis.Axis_collection(Option).t
+val transl_modifier_annots : Parsetree.modes -> _ Transled_modifiers.t
diff --git a/typing/typeopt.ml b/typing/typeopt.ml
index e8b29174ef0..bac12e48cdf 100644
--- a/typing/typeopt.ml
+++ b/typing/typeopt.ml
@@ -328,9 +328,15 @@ let bigarray_specialize_kind_and_layout env ~kind ~layout typ =
   | _ ->
       (kind, layout)
 
-let value_kind_of_value_jkind jkind =
+let value_kind_of_value_jkind env jkind =
   let layout = Jkind.get_layout_defaulting_to_value jkind in
-  let externality_upper_bound = Jkind.get_externality_upper_bound jkind in
+  let type_equal = Ctype.type_equal env in
+  (* In other places, we use [Ctype.type_jkind_purely_if_principal]. Here, we omit
+     the principality check, as we're just trying to compute optimizations. *)
+  let jkind_of_type ty = Some (Ctype.type_jkind_purely env ty) in
+  let externality_upper_bound =
+    Jkind.get_externality_upper_bound ~type_equal ~jkind_of_type jkind
+  in
   match layout, externality_upper_bound with
   | Base Value, External -> Pintval
   | Base Value, External64 ->
@@ -497,7 +503,7 @@ let rec value_kind env ~loc ~visited ~depth ~num_nodes_visited ty
       in
       if cannot_proceed () then
         num_nodes_visited,
-        mk_nn (value_kind_of_value_jkind decl.type_jkind)
+        mk_nn (value_kind_of_value_jkind env decl.type_jkind)
       else
         let visited = Numbers.Int.Set.add (get_id ty) visited in
         (* Default of [Pgenval] is currently safe for the missing cmi fallback
@@ -524,7 +530,7 @@ let rec value_kind env ~loc ~visited ~depth ~num_nodes_visited ty
             "Typeopt.value_kind: non-unary unboxed record can't have kind value"
         | Type_abstract _ ->
           num_nodes_visited,
-          mk_nn (value_kind_of_value_jkind decl.type_jkind)
+          mk_nn (value_kind_of_value_jkind env decl.type_jkind)
         | Type_open -> num_nodes_visited, mk_nn Pgenval
     end
   | Ttuple labeled_fields ->
diff --git a/typing/types.ml b/typing/types.ml
index a745ae47150..d23dc030abf 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -104,14 +104,6 @@ and jkind_l = (allowed * disallowed) jkind
 and jkind_r = (disallowed * allowed) jkind
 and jkind_lr = (allowed * allowed) jkind
 
-(* jkind depends on types defined in this file, but Jkind.equal is required
-   here. When jkind.ml is loaded, it calls set_jkind_equal to fill a ref to the
-   function. *)
-(** Corresponds to [Jkind.equal] *)
-let jkind_equal = ref (fun _ _ ->
-    failwith "jkind_equal should be set by jkind.ml")
-let set_jkind_equal f = jkind_equal := f
-
 module TransientTypeOps = struct
   type t = type_expr
   let compare t1 t2 = t1.id - t2.id
diff --git a/typing/types.mli b/typing/types.mli
index c8613d7e262..3eccf3ba219 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -236,13 +236,6 @@ and jkind_l = (allowed * disallowed) jkind  (* the jkind of an actual type *)
 and jkind_r = (disallowed * allowed) jkind  (* the jkind expected of a type *)
 and jkind_lr = (allowed * allowed) jkind    (* the jkind of a variable *)
 
-(* jkind depends on types defined in this file, but Jkind.equal is required
-   here. When jkind.ml is loaded, it calls set_jkind_equal to fill a ref to the
-   function. *)
-(** INTERNAL USE ONLY
-    jkind.ml should call this with the definition of Jkind.equal *)
-val set_jkind_equal : (jkind_l -> jkind_l -> bool) -> unit
-
 val is_commu_ok: commutable -> bool
 val commu_ok: commutable
 val commu_var: unit -> commutable
diff --git a/utils/misc.ml b/utils/misc.ml
index 7f2ee83b603..db84059a24a 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -530,24 +530,39 @@ module Stdlib = struct
       val ignore_m : 'a t -> unit t
       val all : 'a t list -> 'a list t
       val all_unit : unit t list -> unit t
+
+      module Syntax : sig
+        val (let+) : 'a t -> ('a -> 'b) -> 'b t
+        val (and+) : 'a t -> 'b t -> ('a * 'b) t
+        val (let*) : 'a t -> ('a -> 'b t) -> 'b t
+        val (and*) : 'a t -> 'b t -> ('a * 'b) t
+      end
     end
 
     module type S2 = sig
       type ('a, 'e) t
 
       val bind : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
+      val (>>=) : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
       val return : 'a -> ('a, _) t
       val map : ('a -> 'b) -> ('a, 'e) t -> ('b, 'e) t
       val join : (('a, 'e) t, 'e) t -> ('a, 'e) t
       val ignore_m : (_, 'e) t -> (unit, 'e) t
       val all : ('a, 'e) t list -> ('a list, 'e) t
       val all_unit : (unit, 'e) t list -> (unit, 'e) t
+
+      module Syntax : sig
+        val (let+) : ('a, 'e) t -> ('a -> 'b) -> ('b, 'e) t
+        val (and+) : ('a, 'e) t -> ('b, 'e) t -> ('a * 'b, 'e) t
+        val (let*) : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
+        val (and*) : ('a, 'e) t -> ('b, 'e) t -> ('a * 'b, 'e) t
+      end
     end
 
-    module Make (X : Basic) = struct
+    module[@inline] Make (X : Basic) = struct
       include X
 
-      let ( >>= ) t f = bind t f
+      let[@inline] ( >>= ) t f = bind t f
 
       let map f ma = ma >>= fun a -> return (f a)
 
@@ -564,11 +579,20 @@ module Stdlib = struct
       let rec all_unit = function
         | [] -> return ()
         | t :: ts -> t >>= fun () -> all_unit ts
+
+      module Syntax = struct
+        let[@inline] (let+) t f = map f t
+        let[@inline] (and+) a b = a >>= fun a -> b >>= fun b -> return (a,b)
+        let[@inline] (let*) t f = bind t f
+        let[@inline] (and*) a b = (and+) a b
+      end
     end
 
-    module Make2 (X : Basic2) = struct
+    module[@inline] Make2 (X : Basic2) = struct
       include X
 
+      let[@inline] ( >>= ) t f = bind t f
+
       let map f m =
         bind m (fun a -> return (f a))
 
@@ -586,8 +610,21 @@ module Stdlib = struct
       let rec all_unit = function
         | [] -> return ()
         | m :: ms -> bind m (fun _ -> all_unit ms)
+
+      module Syntax = struct
+        let[@inline] (let+) t f = map f t
+        let[@inline] (and+) a b = a >>= fun a -> b >>= fun b -> return (a,b)
+        let[@inline] (let*) t f = bind t f
+        let[@inline] (and*) a b = (and+) a b
+      end
     end
 
+    module Identity = Make(struct
+        type 'a t = 'a
+        let[@inline] bind x f = f x
+        let[@inline] return x = x
+      end)
+
     module Option = Make(struct
         include Stdlib.Option
         let return = some
diff --git a/utils/misc.mli b/utils/misc.mli
index d9514866457..1111db4807b 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -355,23 +355,40 @@ module Stdlib : sig
           a unit value, all of which are discarded rather than being collected
           into a list. *)
       val all_unit : unit t list -> unit t
+
+      (** As described at https://ocaml.org/manual/latest/bindingops.html *)
+      module Syntax : sig
+        val (let+) : 'a t -> ('a -> 'b) -> 'b t
+        val (and+) : 'a t -> 'b t -> ('a * 'b) t
+        val (let*) : 'a t -> ('a -> 'b t) -> 'b t
+        val (and*) : 'a t -> 'b t -> ('a * 'b) t
+      end
     end
 
     module type S2 = sig
       type ('a, 'e) t
 
       val bind : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
+      val (>>=) : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
       val return : 'a -> ('a, _) t
       val map : ('a -> 'b) -> ('a, 'e) t -> ('b, 'e) t
       val join : (('a, 'e) t, 'e) t -> ('a, 'e) t
       val ignore_m : (_, 'e) t -> (unit, 'e) t
       val all : ('a, 'e) t list -> ('a list, 'e) t
       val all_unit : (unit, 'e) t list -> (unit, 'e) t
+
+      module Syntax : sig
+        val (let+) : ('a, 'e) t -> ('a -> 'b) -> ('b, 'e) t
+        val (and+) : ('a, 'e) t -> ('b, 'e) t -> ('a * 'b, 'e) t
+        val (let*) : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
+        val (and*) : ('a, 'e) t -> ('b, 'e) t -> ('a * 'b, 'e) t
+      end
     end
 
     module Make (X : Basic) : S with type 'a t = 'a X.t
     module Make2 (X : Basic2) : S2 with type ('a, 'e) t = ('a, 'e) X.t
 
+    module Identity : S with type 'a t = 'a
     module Option : S with type 'a t = 'a option
     module Result : S2 with type ('a, 'e) t = ('a, 'e) result
   end