diff --git a/driver/main_args.ml b/driver/main_args.ml
index 4bb52a82494..142f0d65bf2 100644
--- a/driver/main_args.ml
+++ b/driver/main_args.ml
@@ -728,6 +728,10 @@ in
   \    allows a set of extensions, and every successive universe includes \n\
   \    the previous one."
 
+let mk_allow_illegal_crossing f =
+  "-allow-illegal-crossing", Arg.Unit f,
+  "Type declarations will not be checked along the portability or contention axes"
+
 let mk_dump_dir f =
   "-dump-dir", Arg.String f,
   "<dir> dump output like -dlambda into <dir>/<target>.dump"
@@ -920,6 +924,7 @@ module type Common_options = sig
   val _extension : string -> unit
   val _no_extension : string -> unit
   val _extension_universe : string -> unit
+  val _allow_illegal_crossing : unit -> unit
   val _noassert : unit -> unit
   val _nolabels : unit -> unit
   val _nostdlib : unit -> unit
@@ -1201,6 +1206,7 @@ struct
     mk_extension F._extension;
     mk_no_extension F._no_extension;
     mk_extension_universe F._extension_universe;
+    mk_allow_illegal_crossing F._allow_illegal_crossing;
     mk_for_pack_byt F._for_pack;
     mk_g_byt F._g;
     mk_no_g F._no_g;
@@ -1328,6 +1334,7 @@ struct
     mk_extension F._extension;
     mk_no_extension F._no_extension;
     mk_extension_universe F._extension_universe;
+    mk_allow_illegal_crossing F._allow_illegal_crossing;
     mk_noassert F._noassert;
     mk_noinit F._noinit;
     mk_nolabels F._nolabels;
@@ -1421,6 +1428,7 @@ struct
     mk_extension F._extension;
     mk_no_extension F._no_extension;
     mk_extension_universe F._extension_universe;
+    mk_allow_illegal_crossing F._allow_illegal_crossing;
     mk_for_pack_opt F._for_pack;
     mk_g_opt F._g;
     mk_no_g F._no_g;
@@ -1607,6 +1615,7 @@ module Make_opttop_options (F : Opttop_options) = struct
     mk_extension F._extension;
     mk_no_extension F._no_extension;
     mk_extension_universe F._extension_universe;
+    mk_allow_illegal_crossing F._allow_illegal_crossing;
     mk_no_float_const_prop F._no_float_const_prop;
     mk_noassert F._noassert;
     mk_noinit F._noinit;
@@ -1714,6 +1723,7 @@ struct
     mk_extension F._extension;
     mk_no_extension F._no_extension;
     mk_extension_universe F._extension_universe;
+    mk_allow_illegal_crossing F._allow_illegal_crossing;
     mk_noassert F._noassert;
     mk_nolabels F._nolabels;
     mk_nostdlib F._nostdlib;
@@ -1825,6 +1835,7 @@ module Default = struct
     let _no_extension s = Language_extension.(disable_of_string_exn s)
     let _extension_universe s =
       Language_extension.(set_universe_and_enable_all_of_string_exn s)
+    let _allow_illegal_crossing = set Clflags.allow_illegal_crossing
     let _noassert = set noassert
     let _nolabels = set classic
     let _nostdlib = set no_std_include
diff --git a/driver/main_args.mli b/driver/main_args.mli
index 59817e3bf26..992ef1f392a 100644
--- a/driver/main_args.mli
+++ b/driver/main_args.mli
@@ -34,6 +34,7 @@ module type Common_options = sig
   val _extension : string -> unit
   val _no_extension : string -> unit
   val _extension_universe : string -> unit
+  val _allow_illegal_crossing : unit -> unit
   val _noassert : unit -> unit
   val _nolabels : unit -> unit
   val _nostdlib : unit -> unit
diff --git a/testsuite/tests/typing-layouts/allow_illegal_crossing.ml b/testsuite/tests/typing-layouts/allow_illegal_crossing.ml
new file mode 100644
index 00000000000..d22d69b75c0
--- /dev/null
+++ b/testsuite/tests/typing-layouts/allow_illegal_crossing.ml
@@ -0,0 +1,961 @@
+(* TEST
+ {
+   flags = "-allow-illegal-crossing";
+   expect;
+ }
+*)
+
+(*************************************************************************************)
+(* Test 1: nominative types can cross portability and contention axes when annotated *)
+
+type a
+type b : value mod portable = { a : int; b : int }
+[%%expect {|
+type a
+type b : value mod portable = { 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 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
+|}]
+
+module _ = struct
+  type a
+  type b : value mod uncontended = private a
+end
+[%%expect {|
+Line 3, characters 2-44:
+3 |   type b : value mod uncontended = private a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 2, characters 2-8.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 3, characters 2-44.
+|}]
+
+type t : value mod portable uncontended = { a : int; b : int }
+[%%expect {|
+type t : value mod portable uncontended = { a : int; b : int; }
+|}]
+
+type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b }
+[%%expect {|
+type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b; }
+|}]
+
+type t : value mod portable = private { foo : string }
+[%%expect {|
+type t : value mod portable = 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 : 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 t : value mod uncontended = private Foo of int | Bar
+[%%expect {|
+type t : value mod uncontended = 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 : 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
+|}]
+
+module A : sig
+  type t : value mod portable = { a : string }
+end = struct
+  type t = { a : string }
+end
+[%%expect {|
+module A : sig type t : value mod portable = { a : string; } end
+|}]
+
+(********************************************)
+(* Test 2: illegal mode crossing propogates *)
+
+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 portable uncontended = Foo of string
+type ('a : value mod uncontended portable) b
+type c = a b
+|}]
+
+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 portable uncontended = { a : string; b : int; }
+val f : ('a : value mod uncontended portable). 'a -> 'a = <fun>
+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 portable uncontended = { 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 portable uncontended = { 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 portable uncontended = Foo of string | Bar of int
+val x : t = Foo "hello world"
+|}]
+
+module A : sig
+  type t : value mod portable = { a : string }
+end = struct
+  type t = { a : string }
+end
+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
+type ('a : value mod portable) u = 'a
+type v = A.t u
+val x : A.t = {A.a = "hello"}
+|}]
+
+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; }
+val my_str : string = ""
+val y : t = {a = ""}
+|}]
+
+type t : value mod portable = { a : string }
+let my_str : string @@ nonportable = ""
+let y : t @@ portable = { a = my_str }
+[%%expect {|
+type t : value mod portable = { a : string; }
+val my_str : string = ""
+Line 3, characters 30-36:
+3 | let y : t @@ portable = { a = my_str }
+                                  ^^^^^^
+Error: This value is nonportable but expected to be portable.
+|}]
+(* CR layouts v2.8: this is unfortunate that this isn't accepted, but it is fine
+   since pushing the annotation to the right hand side resolves the issue, and
+   -allow-illegal-crossing is a short-term solution *)
+
+type t : value mod uncontended = { a : string }
+let make_str () : string = failwith ""
+let f () =
+  let _ = ({ a = make_str () } : t @@ uncontended) in
+  ()
+[%%expect {|
+type t : value mod uncontended = { a : string; }
+val make_str : unit -> string = <fun>
+val f : unit -> unit = <fun>
+|}]
+
+type t : value mod uncontended = { a : string }
+let make_str () : string = failwith ""
+let f () =
+  let _ : t @@ uncontended = { a = make_str () } in
+  ()
+[%%expect {|
+type t : value mod uncontended = { a : string; }
+val make_str : unit -> string = <fun>
+val f : unit -> unit = <fun>
+|}]
+(* CR layouts v2.8: this is unfortunate that this isn't accepted, but it is fine
+   since pushing the annotation to the right hand side resolves the issue, and
+   -allow-illegal-crossing is a short-term solution *)
+
+type t_value : value
+type t : value mod portable uncontended = Foo of t_value
+let make_value () : t_value = failwith ""
+let f () =
+  let _ = (Foo (make_value ()) : t @@ portable uncontended) in
+  ()
+[%%expect {|
+type t_value : value
+type t : value mod portable uncontended = Foo of t_value
+val make_value : unit -> t_value = <fun>
+val f : unit -> unit = <fun>
+|}]
+
+type t : value mod portable = { a : string }
+let my_str : string @@ nonportable = ""
+let y = ({ a = my_str } : _ @@ portable)
+[%%expect {|
+type t : value mod portable = { a : string; }
+val my_str : string = ""
+Line 3, characters 15-21:
+3 | let y = ({ a = my_str } : _ @@ portable)
+                   ^^^^^^
+Error: This value is nonportable but expected to be portable.
+|}]
+(* CR layouts v2.8: this is unfortunate that this isn't accepted, but it is fine
+   since adding the type to the annotation resolves the issue, and
+   -allow-illegal-crossing is a short-term solution *)
+
+let f (_x : _ @@ portable uncontended) = ()
+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 portable uncontended = Foo of string | Bar of int
+val g : t @ contended -> unit = <fun>
+|}]
+
+(* Demonstrate that -allow-illegal-crossing allows for unsound mode-crossing *)
+module Unsound : sig
+  val cross : 'a @ nonportable contended -> 'a @ portable uncontended
+end = struct
+  type 'a box : value mod portable uncontended = { value : 'a }
+  let cross x =
+    let box = { value = x } in
+    box.value
+end
+
+module Value : sig
+  type t
+  val value : t
+end = struct
+  type t = Foo
+  let value = Foo
+end
+
+let x : Value.t @@ portable uncontended = Unsound.cross Value.value
+[%%expect {|
+module Unsound : sig val cross : 'a @ contended -> 'a @ portable end
+module Value : sig type t val value : t end
+val x : Value.t = <abstr>
+|}]
+
+(* Validate above testing technique *)
+let x : Value.t @@ portable uncontended = Value.value
+[%%expect {|
+Line 1, characters 42-53:
+1 | let x : Value.t @@ portable uncontended = Value.value
+                                              ^^^^^^^^^^^
+Error: This value is nonportable but expected to be portable.
+|}]
+(********************************************************)
+(* Test 3: types cannot cross other axes when annotated *)
+
+type a
+type b : value mod global = private a
+[%%expect {|
+type a
+Line 2, characters 0-37:
+2 | type b : value mod global = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-37.
+|}]
+
+type a
+type b : value mod many = private a
+[%%expect {|
+type a
+Line 2, characters 0-35:
+2 | type b : value mod many = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-35.
+|}]
+
+type a
+type b : value mod unique = private a
+[%%expect {|
+type a
+Line 2, characters 0-37:
+2 | type b : value mod unique = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-37.
+|}]
+
+type a
+type b : immediate = private a
+[%%expect {|
+type a
+Line 2, characters 0-30:
+2 | type b : immediate = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of immediate, because
+         of the definition of b at line 2, characters 0-30.
+|}]
+
+module _ = struct
+  type a
+  type b : value mod global = private a
+end
+[%%expect {|
+Line 3, characters 2-39:
+3 |   type b : value mod global = private a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a/2 is value, because
+         of the definition of a at line 2, characters 2-8.
+       But the layout of type a/2 must be a sublayout of value, because
+         of the definition of b at line 3, characters 2-39.
+|}]
+
+module A : sig
+  type t
+end = struct
+  type t : value mod many = private string
+end
+[%%expect {|
+Line 4, characters 2-42:
+4 |   type t : value mod many = private string
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type string is value, because
+         it is the primitive value type string.
+       But the layout of type string must be a sublayout of value, because
+         of the definition of t at line 4, characters 2-42.
+|}]
+
+type t : value mod external_ = private string
+[%%expect {|
+Line 1, characters 0-45:
+1 | type t : value mod external_ = private string
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type string is value, because
+         it is the primitive value type string.
+       But the layout of type string must be a sublayout of immediate, because
+         of the definition of t at line 1, characters 0-45.
+|}]
+
+type t : value mod global = { a : int; b : int }
+[%%expect {|
+Line 1, characters 0-48:
+1 | type t : value mod global = { a : int; b : int }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type t is value, because
+         it's a boxed record type.
+       But the layout of type t must be a sublayout of value, because
+         of the annotation on the declaration of the type t.
+|}]
+
+type ('a, 'b) t : value mod many = { a : 'a; b : 'b }
+[%%expect {|
+Line 1, characters 0-53:
+1 | type ('a, 'b) t : value mod many = { a : 'a; b : 'b }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type t is value, because
+         it's a boxed record type.
+       But the layout of type t must be a sublayout of value, because
+         of the annotation on the declaration of the type t.
+|}]
+
+type a : value mod unique = private b
+and b
+[%%expect {|
+Line 1, characters 0-37:
+1 | type a : value mod unique = private b
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type b is value, because
+         an abstract type has the value layout by default.
+       But the layout of type b must be a sublayout of value, because
+         of the definition of a at line 1, characters 0-37.
+|}]
+
+type a
+and b : value mod global = private a
+[%%expect {|
+Line 2, characters 0-36:
+2 | and b : value mod global = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a/3 is value, because
+         an abstract type has the value layout by default.
+       But the layout of type a/3 must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-36.
+|}]
+
+module rec A : sig
+  type t : value mod external_
+end = struct
+  type t : value mod external_ = private B.t
+end
+and B : sig
+  type t
+end = struct
+  type t
+end
+[%%expect {|
+Line 4, characters 2-44:
+4 |   type t : value mod external_ = private B.t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type B.t is value, because
+         of the definition of t at line 7, characters 2-8.
+       But the layout of type B.t must be a sublayout of immediate, because
+         of the definition of t at line 4, characters 2-44.
+|}]
+
+module rec A : sig
+  type t
+end = struct
+  type t
+end
+and B : sig
+  type t : value mod many
+end = struct
+  type t : value mod many = private A.t
+end
+[%%expect {|
+Line 9, characters 2-39:
+9 |   type t : value mod many = private A.t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type A.t is value, because
+         of the definition of t at line 2, characters 2-8.
+       But the layout of type A.t must be a sublayout of value, because
+         of the definition of t at line 9, characters 2-39.
+|}]
+
+(*********************************************************************************)
+(* Test 4: types cannot cross portability and contention axes when not annotated *)
+
+module A : sig
+  type t : value mod portable
+end = struct
+  type t = { a : string }
+end
+[%%expect {|
+Lines 3-5, characters 6-3:
+3 | ......struct
+4 |   type t = { a : string }
+5 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig type t = { a : string; } end
+       is not included in
+         sig type t : value mod portable end
+       Type declarations do not match:
+         type t = { a : string; }
+       is not included in
+         type t : value mod portable
+       The layout of the first is value, because
+         of the definition of t at line 4, characters 2-25.
+       But the layout of the first must be a sublayout of value, because
+         of the definition of t at line 2, characters 2-29.
+|}]
+
+module A : sig
+  type t : value mod portable = { a : string }
+end = struct
+  type t = { a : 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 layout of t is value, because
+         of the definition of t at line 4, characters 2-25.
+       But the layout of t must be a sublayout of value, because
+         of the definition of u at line 5, characters 2-39.
+|}]
+
+module A : sig
+  type t : value mod portable = { a : string }
+end = struct
+  type t = { a : string }
+  let x : _ as (_ : value mod portable) = { a = "hello" }
+end
+[%%expect {|
+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 layout of t is value, because
+         of the definition of t at line 4, characters 2-25.
+       But the layout of t must be a sublayout of value, because
+         of the annotation on the wildcard _ at line 5, characters 20-38.
+|}]
+
+type a
+type b : value mod portable = a
+[%%expect {|
+type a
+Line 2, characters 0-31:
+2 | type b : value mod portable = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-31.
+|}]
+
+type a = { foo : int; bar : string }
+type b : any mod portable = a
+[%%expect {|
+type a = { foo : int; bar : string; }
+Line 2, characters 0-29:
+2 | type b : any mod portable = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-36.
+       But the layout of type a must be a sublayout of any, because
+         of the definition of b at line 2, characters 0-29.
+|}]
+
+type a = Foo of int | Bar of string
+type b : any mod uncontended = a
+[%%expect {|
+type a = Foo of int | Bar of string
+Line 2, characters 0-32:
+2 | type b : any mod uncontended = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-35.
+       But the layout of type a must be a sublayout of any, because
+         of the definition of b at line 2, characters 0-32.
+|}]
+
+module Foo : sig
+  type t
+end = struct
+  type t : value mod portable = string
+end
+type t : value mod portable = Foo.t
+[%%expect {|
+Line 4, characters 2-38:
+4 |   type t : value mod portable = string
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type string is value, because
+         it is the primitive value type string.
+       But the layout of type string must be a sublayout of value, because
+         of the definition of t at line 4, characters 2-38.
+|}]
+
+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 layout of type a is value, because
+         of the definition of a at line 1, characters 0-25.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-50.
+|}]
+
+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 layout of type a is value, because
+         of the definition of a at line 1, characters 0-33.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-61.
+|}]
+
+type a = Foo of string | Bar
+type b : value mod uncontended = a = Foo of string | Bar
+[%%expect {|
+type a = Foo of string | Bar
+Line 2, characters 0-56:
+2 | type b : value mod uncontended = a = Foo of string | Bar
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-28.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-56.
+|}]
+
+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
+Line 2, characters 0-61:
+2 | type b : value mod portable = a = private Foo of string | Bar
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-36.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-61.
+|}]
+
+type ('a : value mod uncontended) of_uncontended
+type t = string of_uncontended
+[%%expect {|
+type ('a : value mod uncontended) of_uncontended
+Line 2, characters 9-15:
+2 | type t = string of_uncontended
+             ^^^^^^
+Error: This type string should be an instance of type
+         ('a : value mod uncontended)
+       The layout of string is value, because
+         it is the primitive value type string.
+       But the layout of string must be a sublayout of value, because
+         of the definition of of_uncontended at line 1, characters 0-48.
+|}]
+
+type ('a : value mod portable) of_portable
+type t = { foo : int }
+type u = t of_portable
+[%%expect {|
+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 layout of t is value, because
+         of the definition of t at line 2, characters 0-22.
+       But the layout of t must be a sublayout of value, 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 "hello"
+[%%expect {|
+val f : ('a : value mod portable). 'a -> 'a = <fun>
+Line 2, characters 10-17:
+2 | let _ = f "hello"
+              ^^^^^^^
+Error: This expression has type string but an expression was expected of type
+         ('a : value mod portable)
+       The layout of string is value, because
+         it is the primitive value type string.
+       But the layout of string must be a sublayout of value, because
+         of the definition of f at line 1, characters 4-5.
+|}]
+
+let f : ('a : value mod uncontended). 'a -> 'a = fun x -> x
+let _ = f "hello"
+[%%expect {|
+val f : ('a : value mod uncontended). 'a -> 'a = <fun>
+Line 2, characters 10-17:
+2 | let _ = f "hello"
+              ^^^^^^^
+Error: This expression has type string but an expression was expected of type
+         ('a : value mod uncontended)
+       The layout of string is value, because
+         it is the primitive value type string.
+       But the layout of string must be a sublayout of value, because
+         of the definition of f at line 1, characters 4-5.
+|}]
+
+(* immediate types can still cross *)
+let f : ('a : value mod portable uncontended). 'a -> 'a = fun x -> x
+let _ = f 0
+[%%expect {|
+val f : ('a : value mod uncontended portable). 'a -> 'a = <fun>
+- : int = 0
+|}]
+
+(*****************************************)
+(* Test 5: values cannot illegally cross *)
+
+let x : _ as (_ : value mod portable) = "hello world"
+[%%expect {|
+Line 1, characters 40-53:
+1 | let x : _ as (_ : value mod portable) = "hello world"
+                                            ^^^^^^^^^^^^^
+Error: This expression has type string but an expression was expected of type
+         ('a : value mod portable)
+       The layout of string is value, because
+         it is the primitive value type string.
+       But the layout of string must be a sublayout of value, because
+         of the annotation on the wildcard _ at line 1, characters 18-36.
+|}]
+
+type t = { str : string }
+let f _ : _ as (_ : value mod uncontended) = { str = "hello world" }
+[%%expect {|
+type t = { str : string; }
+Line 2, characters 45-68:
+2 | let f _ : _ as (_ : value mod uncontended) = { str = "hello world" }
+                                                 ^^^^^^^^^^^^^^^^^^^^^^^
+Error: This expression has type t but an expression was expected of type
+         ('a : value mod uncontended)
+       The layout of t is value, because
+         of the definition of t at line 1, characters 0-25.
+       But the layout of t must be a sublayout of value, because
+         of the annotation on the wildcard _ at line 2, characters 20-41.
+|}]
+
+type t = Foo of string
+let f : ('a : value mod portable). 'a -> 'a = fun _ -> Foo "hello world"
+[%%expect {|
+type t = Foo of string
+Line 2, characters 55-72:
+2 | let f : ('a : value mod portable). 'a -> 'a = fun _ -> Foo "hello world"
+                                                           ^^^^^^^^^^^^^^^^^
+Error: This expression has type t but an expression was expected of type
+         ('a : value mod portable)
+       The layout of t is value, because
+         of the definition of t at line 1, characters 0-22.
+       But the layout of t must be a sublayout of value, because
+         of the annotation on the universal variable 'a.
+|}]
+
+type t = string
+let x : ('a : value mod uncontended) = ("hello world" : t)
+[%%expect {|
+type t = string
+Line 2, characters 39-58:
+2 | let x : ('a : value mod uncontended) = ("hello world" : t)
+                                           ^^^^^^^^^^^^^^^^^^^
+Error: This expression has type t = string
+       but an expression was expected of type ('a : value mod uncontended)
+       The layout of t is value, because
+         it is the primitive value type string.
+       But the layout of t must be a sublayout of value, because
+         of the annotation on the type variable 'a.
+|}]
+
+(***************************************)
+(* Test 6: layout check is not ignored *)
+
+type a : word
+type b : value mod portable = a
+[%%expect {|
+type a : word
+Line 2, characters 0-31:
+2 | type b : value mod portable = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is word, because
+         of the definition of a at line 1, characters 0-13.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-31.
+|}]
+
+type a : bits64
+type b : float32 mod uncontended = a
+[%%expect {|
+type a : bits64
+Line 2, characters 0-36:
+2 | type b : float32 mod uncontended = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is bits64, because
+         of the definition of a at line 1, characters 0-15.
+       But the layout of type a must be a sublayout of float32, because
+         of the definition of b at line 2, characters 0-36.
+|}]
+
+type a : any
+type b : value mod uncontended = a
+[%%expect {|
+type a : any
+Line 2, characters 0-34:
+2 | type b : value mod uncontended = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is any, because
+         of the definition of a at line 1, characters 0-12.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-34.
+|}]
+
+(****************************************************************)
+(* Test 7: Non-nominative types cannot perform illegal crossing *)
+
+type a
+type b : value mod portable = a
+[%%expect {|
+type a
+Line 2, characters 0-31:
+2 | type b : value mod portable = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-31.
+|}]
+
+type a
+type b : value mod uncontended = a
+[%%expect {|
+type a
+Line 2, characters 0-34:
+2 | type b : value mod uncontended = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-34.
+|}]
+
+type a
+type b : value mod portable = private a
+[%%expect {|
+type a
+Line 2, characters 0-39:
+2 | type b : value mod portable = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-39.
+|}]
+
+type a
+type b : value mod uncontended = private a
+[%%expect {|
+type a
+Line 2, characters 0-42:
+2 | type b : value mod uncontended = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is value, because
+         of the definition of a at line 1, characters 0-6.
+       But the layout of type a must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-42.
+|}]
+
+type a : word
+type b : any mod uncontended portable = private a
+[%%expect {|
+type a : word
+Line 2, characters 0-49:
+2 | type b : any mod uncontended portable = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is word, because
+         of the definition of a at line 1, characters 0-13.
+       But the layout of type a must be a sublayout of any, because
+         of the definition of b at line 2, characters 0-49.
+|}]
+
+type a : value mod global many unique external_
+type b : immediate = private a
+[%%expect {|
+type a : value mod global many unique external_
+Line 2, characters 0-30:
+2 | type b : immediate = private a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a is immediate, because
+         of the definition of a at line 1, characters 0-47.
+       But the layout of type a must be a sublayout of immediate, because
+         of the definition of b at line 2, characters 0-30.
+|}]
+
+module A : sig
+  type t
+end = struct
+  type t : value mod portable = private string
+end
+[%%expect {|
+Line 4, characters 2-46:
+4 |   type t : value mod portable = private string
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type string is value, because
+         it is the primitive value type string.
+       But the layout of type string must be a sublayout of value, because
+         of the definition of t at line 4, characters 2-46.
+|}]
+
+type a : value mod portable uncontended = private b
+and b
+[%%expect {|
+Line 1, characters 0-51:
+1 | type a : value mod portable uncontended = private b
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type b is value, because
+         an abstract type has the value layout by default.
+       But the layout of type b must be a sublayout of value, because
+         of the definition of a at line 1, characters 0-51.
+|}]
+
+type a
+and b : value mod portable uncontended = a
+[%%expect {|
+Line 2, characters 0-42:
+2 | and b : value mod portable uncontended = a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type a/2 is value, because
+         an abstract type has the value layout by default.
+       But the layout of type a/2 must be a sublayout of value, because
+         of the definition of b at line 2, characters 0-42.
+|}]
+
+module rec A : sig
+  type t : value mod portable uncontended
+end = struct
+  type t : value mod portable uncontended = B.t
+end
+and B : sig
+  type t
+end = struct
+  type t
+end
+[%%expect {|
+Line 4, characters 2-47:
+4 |   type t : value mod portable uncontended = B.t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type B.t is value, because
+         of the definition of t at line 7, characters 2-8.
+       But the layout of type B.t must be a sublayout of value, because
+         of the definition of t at line 4, characters 2-47.
+|}]
+
+module rec A : sig
+  type t
+end = struct
+  type t
+end
+and B : sig
+  type t : value mod portable uncontended
+end = struct
+  type t : value mod portable uncontended = private A.t
+end
+[%%expect {|
+Line 9, characters 2-55:
+9 |   type t : value mod portable uncontended = private A.t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type A.t is value, because
+         of the definition of t at line 2, characters 2-8.
+       But the layout of type A.t must be a sublayout of value, because
+         of the definition of t at line 9, characters 2-55.
+|}]
diff --git a/testsuite/tests/typing-layouts/jkinds.ml b/testsuite/tests/typing-layouts/jkinds.ml
index 59cc25fd4b8..c9ff191ab1f 100644
--- a/testsuite/tests/typing-layouts/jkinds.ml
+++ b/testsuite/tests/typing-layouts/jkinds.ml
@@ -1565,3 +1565,113 @@ Error: This expression has type <  > but an expression was expected of type
 |}]
 (* CR layouts v2.8: Bad error message. The error message should be about a kind or mode
    mismatch, not a layout mismatch. *)
+
+(****************************************)
+(* Test 11: Inference of type parameter *)
+
+type 'a t : any = 'a
+[%%expect {|
+type 'a t = 'a
+|}]
+
+type 'a t : value = 'a
+[%%expect {|
+type 'a t = 'a
+|}]
+
+type 'a t : value mod global = 'a
+[%%expect {|
+Line 1, characters 0-33:
+1 | type 'a t : value mod global = 'a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type 'a is value, because
+         of the definition of t at line 1, characters 0-33.
+       But the layout of type 'a must be a sublayout of value, because
+         of the definition of t at line 1, characters 0-33.
+|}]
+(* CR layouts v2.8: this should be accepted; 'a should be inferred to have kind
+   value mod global *)
+
+type 'a t : word = 'a
+[%%expect {|
+Line 1, characters 0-21:
+1 | type 'a t : word = 'a
+    ^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type 'a is value, because
+         of the definition of t at line 1, characters 0-21.
+       But the layout of type 'a must be a sublayout of word, because
+         of the definition of t at line 1, characters 0-21.
+|}]
+(* CR layouts v2.8: this should be accepted; 'a should be inferred to have kind
+   word *)
+
+type 'a t : any = private 'a
+[%%expect {|
+type 'a t = private 'a
+|}]
+
+type 'a t : value = private 'a
+[%%expect {|
+type 'a t = private 'a
+|}]
+
+type 'a t : value mod global = private 'a
+[%%expect {|
+Line 1, characters 0-41:
+1 | type 'a t : value mod global = private 'a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type 'a is value, because
+         of the definition of t at line 1, characters 0-41.
+       But the layout of type 'a must be a sublayout of value, because
+         of the definition of t at line 1, characters 0-41.
+|}]
+(* CR layouts v2.8: this should be accepted; 'a should be inferred to have kind
+  value mod global *)
+
+type 'a t : word = private 'a
+[%%expect {|
+Line 1, characters 0-29:
+1 | type 'a t : word = private 'a
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type 'a is value, because
+         of the definition of t at line 1, characters 0-29.
+       But the layout of type 'a must be a sublayout of word, because
+         of the definition of t at line 1, characters 0-29.
+|}]
+(* CR layouts v2.8: this should be accepted; 'a should be inferred to have kind
+  word *)
+
+type 'a t : value mod global = Foo of 'a [@@unboxed]
+[%%expect {|
+Line 1, characters 0-52:
+1 | type 'a t : value mod global = Foo of 'a [@@unboxed]
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type t is value, because
+         it instantiates an unannotated type parameter of t, defaulted to layout value.
+       But the layout of type t must be a sublayout of value, because
+         of the annotation on the declaration of the type t.
+|}]
+(* CR layouts v2.8: this should be accepted; 'a should be inferred to have kind
+  value mod global *)
+
+type 'a t : value mod global = { x : 'a }
+[%%expect {|
+Line 1, characters 0-41:
+1 | type 'a t : value mod global = { x : 'a }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type t is value, because
+         it's a boxed record type.
+       But the layout of type t must be a sublayout of value, because
+         of the annotation on the declaration of the type t.
+|}]
+
+type 'a t : value mod many = { x : 'a }
+[%%expect {|
+Line 1, characters 0-39:
+1 | type 'a t : value mod many = { x : 'a }
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The layout of type t is value, because
+         it's a boxed record type.
+       But the layout of type t must be a sublayout of value, because
+         of the annotation on the declaration of the type t.
+|}]
diff --git a/typing/ctype.ml b/typing/ctype.ml
index f1740a7cb80..4a92475cfd9 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1344,6 +1344,7 @@ let new_local_type ?(loc = Location.none) ?manifest_and_scope jkind ~jkind_annot
     type_attributes = [];
     type_unboxed_default = false;
     type_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
+    type_has_illegal_crossings = false;
   }
 
 let existential_name cstr ty =
@@ -6491,6 +6492,7 @@ let nondep_type_decl env mid is_covariant decl =
       type_attributes = decl.type_attributes;
       type_unboxed_default = decl.type_unboxed_default;
       type_uid = decl.type_uid;
+      type_has_illegal_crossings = decl.type_has_illegal_crossings;
     }
   with Nondep_cannot_erase _ as exn ->
     clear_hash ();
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index f19d23b4b66..a1f6ca2e372 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -91,6 +91,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep =
           type_attributes = [];
           type_unboxed_default = false;
           type_uid = Uid.mk ~current_unit;
+          type_has_illegal_crossings = false;
         }
       in
       existentials,
diff --git a/typing/jkind.ml b/typing/jkind.ml
index 02e6db420fa..0e7c4baf6ad 100644
--- a/typing/jkind.ml
+++ b/typing/jkind.ml
@@ -800,6 +800,30 @@ module Jkind_desc = struct
       externality_upper_bound = Externality.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
+    in
+    let new_contention =
+      Contention.Const.meet t.modes_upper_bounds.contention
+        from.modes_upper_bounds.contention
+    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)
+    in
+    ( { t with
+        modes_upper_bounds =
+          { t.modes_upper_bounds with
+            portability = new_portability;
+            contention = new_contention
+          }
+      },
+      added_crossings )
+
   let max = of_const Const.max
 
   let equate_or_equal ~allow_mutation
@@ -1029,6 +1053,12 @@ end
 let add_mode_crossing t =
   { t with jkind = Jkind_desc.add_mode_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
+
 (*** extension requirements ***)
 (* The [annotation_context] parameter can be used to allow annotations / kinds
    in different contexts to be enabled with different extension settings.
diff --git a/typing/jkind.mli b/typing/jkind.mli
index 50e37193e15..37266d8cfed 100644
--- a/typing/jkind.mli
+++ b/typing/jkind.mli
@@ -298,6 +298,11 @@ end
 (** Take an existing [t] and add an ability to mode-cross along all the axes. *)
 val add_mode_crossing : t -> t
 
+(** 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:t -> t -> t * bool
+
 (******************************)
 (* construction *)
 
diff --git a/typing/predef.ml b/typing/predef.ml
index 288cec7013e..6b3b0b9c9d8 100644
--- a/typing/predef.ml
+++ b/typing/predef.ml
@@ -231,6 +231,7 @@ let mk_add_type add_type
      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
@@ -269,6 +270,7 @@ let build_initial_env add_type add_extension empty_env =
        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
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index c50487ee75a..3f6ff717c17 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -40,7 +40,7 @@ module Sig_component_kind = Shape.Sig_component_kind
    [type 'a t : <<this one>> = ...].
 
    We print the jkind when it cannot be inferred from the rest of what is
-   printed. Specifically, we print the user-written jkind in both of these
+   printed. Specifically, we print the user-written jkind in any of these
    cases:
 
    (C1.1) The type declaration is abstract and has no manifest (i.e.,
@@ -54,6 +54,10 @@ module Sig_component_kind = Shape.Sig_component_kind
    be impossible to deduce the jkind.  We thus defer to the user in determining
    whether to print the jkind annotation.
 
+   (* CR layouts v2.8: remove this case *)
+   (C1.3) The type has illegal mode crossings. In this case, the jkind is overridden by
+   the user rather than being inferred from the definition.
+
    Case (C2). The jkind on a type parameter to a type, like
    [type ('a : <<this one>>) t = ...].
 
@@ -1875,11 +1879,12 @@ let tree_of_type_decl id decl =
   in
   (* The algorithm for setting [lay] here is described as Case (C1) in
      Note [When to print jkind annotations] *)
-  let jkind_annotation = match ty, unboxed with
-    | (Otyp_abstract, _) | (_, true) ->
+  let jkind_annotation = match ty, unboxed, decl.type_has_illegal_crossings with
+    | (Otyp_abstract, _, _) | (_, true, _) | (_, _, true) ->
         (* The two cases of (C1) from the Note correspond to Otyp_abstract.
            Anything but the default must be user-written, so we print the
            user-written annotation. *)
+        (* type_has_illegal_crossings corresponds to C1.3 *)
         decl.type_jkind_annotation
     | _ -> None (* other cases have no jkind annotation *)
   in
@@ -2338,6 +2343,7 @@ let dummy =
     type_attributes = [];
     type_unboxed_default = false;
     type_uid = Uid.internal_not_actually_unique;
+    type_has_illegal_crossings = false;
   }
 
 (** we hide items being defined from short-path to avoid shortening
diff --git a/typing/subst.ml b/typing/subst.ml
index 27d8ccd4b63..8f5c9d5bc2a 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -503,6 +503,7 @@ let type_declaration' copy_scope s decl =
     type_attributes = attrs s decl.type_attributes;
     type_unboxed_default = decl.type_unboxed_default;
     type_uid = decl.type_uid;
+    type_has_illegal_crossings = decl.type_has_illegal_crossings;
   }
 
 let type_declaration s decl =
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 4caaf005ad0..403a0e6c654 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -1619,6 +1619,7 @@ let temp_abbrev loc id arity uid =
        type_attributes = []; (* or keep attrs from the class decl? *)
        type_unboxed_default = false;
        type_uid = uid;
+       type_has_illegal_crossings = false;
       }
   in
   (!params, ty, ty_td)
@@ -1850,6 +1851,7 @@ let class_infos define_class kind
      type_attributes = []; (* or keep attrs from cl? *)
      type_unboxed_default = false;
      type_uid = dummy_class.cty_uid;
+     type_has_illegal_crossings = false;
     }
   in
   let (cl_params, cl_ty) =
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 491f720bf8f..c807f370971 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -282,6 +282,7 @@ let enter_type ?abstract_abbrevs rec_flag env sdecl (id, uid) =
       type_attributes = sdecl_attributes;
       type_unboxed_default = false;
       type_uid = uid;
+      type_has_illegal_crossings = false;
     }
   in
   add_type ~check:true id decl env
@@ -928,6 +929,7 @@ let transl_declaration env sdecl (id, uid) =
         type_attributes = sdecl_attributes;
         type_unboxed_default = unboxed_default;
         type_uid = uid;
+        type_has_illegal_crossings = false;
       } in
   (* Check constraints *)
     List.iter
@@ -1112,6 +1114,14 @@ let check_coherence env loc dpath decl =
   match decl with
     { type_kind = (Type_variant _ | Type_record _| Type_open);
       type_manifest = Some ty } ->
+      if !Clflags.allow_illegal_crossing then begin 
+        let jkind' = Ctype.type_jkind_purely env ty in
+        begin match Jkind.sub_with_history jkind' decl.type_jkind with
+        | Ok _ -> ()
+        | Error v ->
+          raise (Error (loc, Jkind_mismatch_of_type (ty,v)))
+        end
+      end;
       begin match get_desc ty with
         Tconstr(path, args, _) ->
           begin try
@@ -1590,6 +1600,12 @@ let update_decl_jkind env dpath decl =
       assert false
   in
 
+  let add_crossings jkind =
+    match !Clflags.allow_illegal_crossing with
+    | true -> Jkind.add_portability_and_contention_crossing ~from:decl.type_jkind jkind
+    | false -> jkind, false
+  in
+
   let new_decl, new_jkind = match decl.type_kind with
     | Type_abstract _ -> decl, decl.type_jkind
     | Type_open ->
@@ -1597,11 +1613,17 @@ let update_decl_jkind env dpath decl =
       { decl with type_jkind }, type_jkind
     | Type_record (lbls, rep) ->
       let lbls, rep, type_jkind = update_record_kind decl.type_loc lbls rep in
-      { decl with type_kind = Type_record (lbls, rep); type_jkind },
+      let type_jkind, type_has_illegal_crossings = add_crossings type_jkind in
+      { decl with type_kind = Type_record (lbls, rep);
+                  type_jkind;
+                  type_has_illegal_crossings },
       type_jkind
     | Type_variant (cstrs, rep) ->
       let cstrs, rep, type_jkind = update_variant_kind cstrs rep in
-      { decl with type_kind = Type_variant (cstrs, rep); type_jkind },
+      let type_jkind, type_has_illegal_crossings = add_crossings type_jkind in
+      { decl with type_kind = Type_variant (cstrs, rep);
+                  type_jkind;
+                  type_has_illegal_crossings },
       type_jkind
   in
 
@@ -3095,6 +3117,7 @@ let transl_with_constraint id ?fixed_row_path ~sig_env ~sig_decl ~outer_env
       type_attributes = sdecl.ptype_attributes;
       type_unboxed_default;
       type_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
+      type_has_illegal_crossings = false;
     }
   in
   Option.iter (fun p -> set_private_row env sdecl.ptype_loc p new_sig_decl)
@@ -3135,6 +3158,7 @@ let transl_with_constraint id ?fixed_row_path ~sig_env ~sig_decl ~outer_env
 
       type_variance = new_type_variance;
       type_separability = new_type_separability;
+      type_has_illegal_crossings = false;
     } in
   {
     typ_id = id;
@@ -3173,7 +3197,8 @@ let transl_package_constraint ~loc ty =
     type_loc = loc;
     type_attributes = [];
     type_unboxed_default = false;
-    type_uid = Uid.mk ~current_unit:(Env.get_unit_name ())
+    type_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
+    type_has_illegal_crossings = false;
   }
 
 (* Approximate a type declaration: just make all types abstract *)
@@ -3197,6 +3222,7 @@ let abstract_type_decl ~injective ~jkind ~jkind_annotation ~params =
       type_attributes = [];
       type_unboxed_default = false;
       type_uid = Uid.internal_not_actually_unique;
+      type_has_illegal_crossings = false;
     }
   end
 
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 78a97563491..3637a3bf950 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -682,6 +682,7 @@ let merge_constraint initial_env loc sg lid constr =
             type_attributes = [];
             type_unboxed_default = false;
             type_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
+            type_has_illegal_crossings = false;
           }
         and id_row = Ident.create_local (s^"#row") in
         let initial_env =
diff --git a/typing/types.ml b/typing/types.ml
index 2510e87056f..e39162eecda 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -265,6 +265,7 @@ type type_declaration =
     type_attributes: Parsetree.attributes;
     type_unboxed_default: bool;
     type_uid: Uid.t;
+    type_has_illegal_crossings: bool;
  }
 
 and type_decl_kind = (label_declaration, constructor_declaration) type_kind
diff --git a/typing/types.mli b/typing/types.mli
index 42f0950df2b..61c93e5f39b 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -532,6 +532,10 @@ type type_declaration =
     type_unboxed_default: bool;
     (* true if the unboxed-ness of this type was chosen by a compiler flag *)
     type_uid: Uid.t;
+    type_has_illegal_crossings: bool;
+    (* true iff the type definition has illegal crossings of the portability and
+       contention axes *)
+    (* CR layouts v2.8: remove type_has_illegal_crossings *)
   }
 
 and type_decl_kind = (label_declaration, constructor_declaration) type_kind
diff --git a/utils/clflags.ml b/utils/clflags.ml
index fd001b6a896..f8af7531223 100644
--- a/utils/clflags.ml
+++ b/utils/clflags.ml
@@ -202,6 +202,7 @@ let afl_inst_ratio = ref 100           (* -afl-inst-ratio *)
 
 let function_sections = ref false      (* -function-sections *)
 let probes = ref Config.probes         (* -probes *)
+let allow_illegal_crossing = ref false (* -allow_illegal_crossing *)
 let simplify_rounds = ref None        (* -rounds *)
 let default_simplify_rounds = ref 1        (* -rounds *)
 let rounds () =
diff --git a/utils/clflags.mli b/utils/clflags.mli
index ea7c00116b6..b75d282c959 100644
--- a/utils/clflags.mli
+++ b/utils/clflags.mli
@@ -218,6 +218,7 @@ val afl_instrument : bool ref
 val afl_inst_ratio : int ref
 val function_sections : bool ref
 val probes : bool ref
+val allow_illegal_crossing : bool ref
 
 val all_passes : string list ref
 val dumped_pass : string -> bool