diff --git a/otherlibs/stdlib_alpha/capsule.ml b/otherlibs/stdlib_alpha/capsule.ml
index ef6e17cf201..58707f5d7d8 100644
--- a/otherlibs/stdlib_alpha/capsule.ml
+++ b/otherlibs/stdlib_alpha/capsule.ml
@@ -86,7 +86,7 @@ module Password : sig
     type 'k t : value mod many portable contended
 
     (* Can break the soundness of the API. *)
-    val unsafe_mk : unit -> 'k t @ local @@ portable
+    val unsafe_mk : unit -> 'k t @ local unyielding @@ portable
     val id : 'k t @ local -> 'k Id.t @@ portable
   end
 
@@ -131,7 +131,7 @@ end = struct
          | already_set_id -> already_set_id)
       | set_id -> set_id
 
-    let unsafe_mk () : _ @@ local = A.make Id.uninitialized
+    let unsafe_mk () : _ @@ local unyielding = A.make Id.uninitialized
   end
 
   let[@inline] shared t = t
@@ -405,13 +405,13 @@ module Key : sig
 
   val with_password_shared :
     'k t
-    -> ('k Password.Shared.t @ local -> 'a) @ local
+    -> ('k Password.Shared.t @ local unyielding -> 'a) @ local
     -> 'a
     @@ portable
 
   val with_password_shared_local :
     'k t
-    -> ('k Password.Shared.t @ local -> 'a @ local) @ local
+    -> ('k Password.Shared.t @ local unyielding -> 'a @ local) @ local
     -> 'a @ local
     @@ portable
 
@@ -680,7 +680,7 @@ module Rwlock = struct
   let[@inline] with_read_lock :
     type k.
     k t
-    -> (k Password.Shared.t @ local -> 'a) @ local
+    -> (k Password.Shared.t @ local unyielding -> 'a) @ local
     -> 'a
     @@ portable
     = fun t f ->
diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml
index bfbe352a3d8..6398f5a0e0e 100644
--- a/testsuite/tests/typing-jkind-bounds/basics.ml
+++ b/testsuite/tests/typing-jkind-bounds/basics.ml
@@ -1157,15 +1157,7 @@ Error: The kind of type "t" is value
 type 'a t : value mod global portable contended many aliased unyielding =
   { x : 'a @@ global portable contended many aliased } [@@unboxed]
 [%%expect {|
-Lines 1-2, characters 0-66:
-1 | type 'a t : value mod global portable contended many aliased unyielding =
-2 |   { x : 'a @@ global portable contended many aliased } [@@unboxed]
-Error: The kind of type "t" is value mod global aliased many contended portable
-         because it instantiates an unannotated type parameter of t,
-         chosen to have kind value mod global aliased many contended portable.
-       But the kind of type "t" must be a subkind of
-         immutable_data mod global aliased
-         because of the annotation on the declaration of the type t.
+type 'a t = { global_ x : 'a @@ many portable aliased contended; } [@@unboxed]
 |}]
 (* CR layouts v2.8: this could be accepted, if we infer ('a : value mod
    unyielding). We do not currently do this, because we finish inference of the
@@ -1191,7 +1183,7 @@ Error: The kind of type "t" is value
          because it instantiates an unannotated type parameter of t,
          chosen to have kind value.
        But the kind of type "t" must be a subkind of
-         immutable_data mod global aliased
+         immutable_data mod global aliased yielding
          because of the annotation on the declaration of the type t.
 |}]
 (* CR layouts v2.8: this should be accepted *)
@@ -1264,10 +1256,13 @@ 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 immutable_data with 'a
+Error: The kind of type "t" is immutable_data with 'a @@ unyielding
          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.
+
+       The first mode-crosses less than the second along:
+         locality: mod local ≰ mod global
 |}]
 
 (*****************************)
@@ -1443,7 +1438,7 @@ Line 1, characters 41-51:
                                              ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod aliased)"
-       The kind of <  > is value mod global many unyielding
+       The kind of <  > is value mod global many
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod aliased
          because of the annotation on the wildcard _ at line 1, characters 19-36.
@@ -1456,7 +1451,7 @@ Line 1, characters 42-52:
                                               ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of <  > is value mod global many unyielding
+       The kind of <  > is value mod global many
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod portable
          because of the annotation on the wildcard _ at line 1, characters 19-37.
@@ -1469,7 +1464,7 @@ Line 1, characters 43-53:
                                                ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod contended)"
-       The kind of <  > is value mod global many unyielding
+       The kind of <  > is value mod global many
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod contended
          because of the annotation on the wildcard _ at line 1, characters 19-38.
@@ -1482,7 +1477,7 @@ Line 1, characters 43-53:
                                                ^^^^^^^^^^
 Error: This expression has type "<  >" but an expression was expected of type
          "('a : value mod external_)"
-       The kind of <  > is value mod global many unyielding
+       The kind of <  > is value mod global many
          because it's the type of an object.
        But the kind of <  > must be a subkind of value mod external_
          because of the annotation on the wildcard _ at line 1, characters 19-38.
diff --git a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml
index ee08dc78feb..542067d7984 100644
--- a/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml
+++ b/testsuite/tests/typing-jkind-bounds/subsumption/modalities.ml
@@ -124,8 +124,7 @@ end = struct
   type 'a t : immediate with 'a @@ aliased many contended global portable
 end
 [%%expect {|
-module M :
-  sig type 'a t : value mod global aliased many contended portable end
+module M : sig type 'a t : immutable_data mod global aliased yielding end
 |}]
 
 module M : sig
diff --git a/testsuite/tests/typing-layouts-products/basics_alpha.ml b/testsuite/tests/typing-layouts-products/basics_alpha.ml
index ecab40ae64e..4c0e1a68484 100644
--- a/testsuite/tests/typing-layouts-products/basics_alpha.ml
+++ b/testsuite/tests/typing-layouts-products/basics_alpha.ml
@@ -67,11 +67,9 @@ Line 3, characters 0-39:
 3 | type t3 : any mod non_null = #(t1 * t2);;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
-         any_non_null mod global aliased many contended portable unyielding
-                          external_
+         any_non_null mod global aliased many contended portable external_
          with t1 with t2
-         & any_non_null mod global aliased many contended portable unyielding
-                            external_
+         & any_non_null mod global aliased many contended portable external_
          with t1 with t2
          because it is an unboxed tuple.
        But the kind of type "#(t1 * t2)" must be a subkind of any_non_null
@@ -88,11 +86,9 @@ Line 3, characters 0-45:
 3 | type t3 : any & any mod non_null = #(t1 * t2);;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
-         any_non_null mod global aliased many contended portable unyielding
-                          external_
+         any_non_null mod global aliased many contended portable external_
          with t1 with t2
-         & any_non_null mod global aliased many contended portable unyielding
-                            external_
+         & any_non_null mod global aliased many contended portable external_
          with t1 with t2
          because it is an unboxed tuple.
        But the kind of type "#(t1 * t2)" must be a subkind of
@@ -110,11 +106,9 @@ Line 3, characters 0-62:
 3 | type t3 : (any mod non_null) & (any mod non_null) = #(t1 * t2);;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "#(t1 * t2)" is
-         any_non_null mod global aliased many contended portable unyielding
-                          external_
+         any_non_null mod global aliased many contended portable external_
          with t1 with t2
-         & any_non_null mod global aliased many contended portable unyielding
-                            external_
+         & any_non_null mod global aliased many contended portable external_
          with t1 with t2
          because it is an unboxed tuple.
        But the kind of type "#(t1 * t2)" must be a subkind of
diff --git a/testsuite/tests/typing-layouts/allow_any.ml b/testsuite/tests/typing-layouts/allow_any.ml
index 62c31a943f3..25b4fd0ff9c 100644
--- a/testsuite/tests/typing-layouts/allow_any.ml
+++ b/testsuite/tests/typing-layouts/allow_any.ml
@@ -313,7 +313,7 @@ module B = struct
   let a t = t.a
 end
 [%%expect{|
-module A : sig type t : mutable_data mod global external_ end
+module A : sig type t : mutable_data mod global external_ yielding end
 module B :
   sig
     type t : value mod contended portable = { a : A.t; }
diff --git a/testsuite/tests/typing-layouts/hash_types.ml b/testsuite/tests/typing-layouts/hash_types.ml
index 92ce2dabe16..d2d45261a2a 100644
--- a/testsuite/tests/typing-layouts/hash_types.ml
+++ b/testsuite/tests/typing-layouts/hash_types.ml
@@ -217,7 +217,7 @@ type r = { i : int ; mutable s : string }
 type u = r# = #{ i : int ; s : string @@ global many aliased unyielding }
 [%%expect{|
 type r = { i : int; mutable s : string; }
-type u = r# = #{ i : int; global_ s : string @@ many unyielding aliased; }
+type u = r# = #{ i : int; global_ s : string @@ many aliased; }
 |}]
 
 (*******************)
diff --git a/testsuite/tests/typing-modes/lazy.ml b/testsuite/tests/typing-modes/lazy.ml
index fd834b214e5..27f7993ee57 100644
--- a/testsuite/tests/typing-modes/lazy.ml
+++ b/testsuite/tests/typing-modes/lazy.ml
@@ -28,6 +28,16 @@ Line 2, characters 18-19:
 Error: The value "x" is local, so cannot be used inside a lazy expression.
 |}]
 
+(* For simplicity, we also require them to be [unyielding]. *)
+let foo (x @ yielding) =
+    lazy (let _ = x in ())
+[%%expect{|
+Line 2, characters 18-19:
+2 |     lazy (let _ = x in ())
+                      ^
+Error: The value "x" is yielding, so cannot be used inside a lazy expression that may not yield.
+|}]
+
 (* lazy expression is constructed as global *)
 let foo () =
     lazy ("hello")
diff --git a/testsuite/tests/typing-modes/yielding.ml b/testsuite/tests/typing-modes/yielding.ml
index e472f807124..e4daa9206e7 100644
--- a/testsuite/tests/typing-modes/yielding.ml
+++ b/testsuite/tests/typing-modes/yielding.ml
@@ -18,7 +18,7 @@ let with_effect : ((string -> unit) @ local yielding -> 'a) -> 'a =
 
 [%%expect{|
 val storage : string ref = {contents = ""}
-val with_effect : (local_ (string -> unit) @ yielding -> 'a) -> 'a = <fun>
+val with_effect : (local_ (string -> unit) -> 'a) -> 'a = <fun>
 |}]
 
 let () = with_effect (fun k -> k "Hello, world!")
@@ -36,7 +36,7 @@ let () = with_effect (fun k -> run_yielding k)
 let _ = !storage
 
 [%%expect{|
-val run_yielding : local_ (string -> unit) @ yielding -> unit = <fun>
+val run_yielding : local_ (string -> unit) -> unit = <fun>
 - : string = "my string"
 |}]
 
@@ -45,25 +45,19 @@ let run_unyielding : (string -> unit) @ local unyielding -> unit = fun f -> f "a
 let () = with_effect (fun k -> run_unyielding k)
 
 [%%expect{|
-val run_unyielding : local_ (string -> unit) -> unit = <fun>
+val run_unyielding : local_ (string -> unit) @ unyielding -> unit = <fun>
 Line 3, characters 46-47:
 3 | let () = with_effect (fun k -> run_unyielding k)
                                                   ^
 Error: This value is "yielding" but expected to be "unyielding".
 |}]
 
-(* CR dkalinichenko: default [local] arguments to [yielding]. *)
-
 let run_default : (string -> unit) @ local -> unit = fun f -> f "some string"
 
 let () = with_effect (fun k -> run_default k)
 
 [%%expect{|
 val run_default : local_ (string -> unit) -> unit = <fun>
-Line 3, characters 43-44:
-3 | let () = with_effect (fun k -> run_default k)
-                                               ^
-Error: This value is "yielding" but expected to be "unyielding".
 |}]
 
 (* A closure over a [yielding] value must be [yielding]. *)
@@ -78,3 +72,207 @@ Line 2, characters 45-46:
                                                  ^
 Error: The value "k" is yielding, so cannot be used inside a function that may not yield.
 |}]
+
+
+type 'a t1 = Mk1 of 'a @@ global
+
+type 'a t2 = Mk2 of 'a @@ global yielding
+
+type 'a t3 = Mk3 of 'a @@ unyielding
+
+type 'a t4 = Mk4 of 'a @@ yielding
+
+let with_global_effect : ((string -> unit) @ yielding -> 'a) -> 'a =
+  fun f -> f ((:=) storage)
+
+[%%expect{|
+type 'a t1 = Mk1 of global_ 'a
+type 'a t2 = Mk2 of global_ 'a @@ yielding
+type 'a t3 = Mk3 of 'a @@ unyielding
+type 'a t4 = Mk4 of 'a
+val with_global_effect : ((string -> unit) @ yielding -> 'a) -> 'a = <fun>
+|}]
+
+(* [global] modality implies [unyielding]. *)
+let _ = with_global_effect (fun k -> let _ = Mk1 k in ())
+
+[%%expect{|
+Line 1, characters 49-50:
+1 | let _ = with_global_effect (fun k -> let _ = Mk1 k in ())
+                                                     ^
+Error: This value is "yielding" but expected to be "unyielding".
+|}]
+
+(* [global yielding] works: *)
+let _ = with_global_effect (fun k -> let _ = Mk2 k in ())
+
+[%%expect{|
+- : unit = ()
+|}]
+
+(* [unyielding] and [yielding] modalities: *)
+let _ = with_global_effect (fun k -> let _ = Mk3 k in ())
+
+[%%expect{|
+Line 1, characters 49-50:
+1 | let _ = with_global_effect (fun k -> let _ = Mk3 k in ())
+                                                     ^
+Error: This value is "yielding" but expected to be "unyielding".
+|}]
+
+let _ = with_global_effect (fun k -> let _ = Mk4 k in ())
+
+[%%expect{|
+- : unit = ()
+|}]
+
+(* Externals and [yielding]: *)
+
+external ok_yielding : 'a @ local -> unit = "%ignore"
+
+let _ = ok_yielding 4
+
+let _ = ok_yielding (stack_ (Some "local string"))
+
+let _ = with_global_effect (fun k -> ok_yielding k)
+
+[%%expect{|
+external ok_yielding : local_ 'a -> unit = "%ignore"
+- : unit = ()
+- : unit = ()
+- : unit = ()
+|}]
+
+external requires_unyielding : 'a @ local unyielding -> unit = "%ignore"
+
+let _ = requires_unyielding 4
+
+let _ = requires_unyielding (stack_ (Some "local string"))
+
+let _ = with_global_effect (fun k -> requires_unyielding k)
+
+[%%expect{|
+external requires_unyielding : local_ 'a @ unyielding -> unit = "%ignore"
+- : unit = ()
+- : unit = ()
+Line 7, characters 57-58:
+7 | let _ = with_global_effect (fun k -> requires_unyielding k)
+                                                             ^
+Error: This value is "yielding" but expected to be "unyielding".
+|}]
+
+external returns_unyielding : 'a -> 'a @ local unyielding = "%identity"
+
+let _ = requires_unyielding (returns_unyielding "some string")
+
+[%%expect{|
+external returns_unyielding : 'a -> local_ 'a @ unyielding = "%identity"
+- : unit = ()
+|}]
+
+(* [@local_opt] and [yielding]: *)
+
+external id : ('a[@local_opt]) -> ('a[@local_opt]) = "%identity"
+
+let f1 x = id x
+let f2 (x @ local) = exclave_ id x
+let f3 (x @ yielding) = id x
+let f4 (x @ local unyielding) = exclave_ id x
+
+[%%expect{|
+external id : ('a [@local_opt]) -> ('a [@local_opt]) = "%identity"
+val f1 : 'a -> 'a = <fun>
+val f2 : local_ 'a -> local_ 'a = <fun>
+val f3 : 'a @ yielding -> 'a @ yielding = <fun>
+val f4 : local_ 'a @ unyielding -> local_ 'a = <fun>
+|}]
+
+(* Test [instance_prim] + mixed mode annots. *)
+external requires_unyielding : 'a @ local unyielding -> (unit [@local_opt]) = "%ignore"
+
+let f1 x = requires_unyielding x
+[%%expect{|
+external requires_unyielding : local_ 'a @ unyielding -> (unit [@local_opt])
+  = "%ignore"
+val f1 : 'a -> unit = <fun>
+|}]
+
+let f2 (x @ local) = exclave_ requires_unyielding x
+
+[%%expect{|
+Line 1, characters 50-51:
+1 | let f2 (x @ local) = exclave_ requires_unyielding x
+                                                      ^
+Error: This value is "yielding" but expected to be "unyielding".
+|}]
+
+let f3 (x @ yielding) = requires_unyielding x
+[%%expect{|
+Line 1, characters 44-45:
+1 | let f3 (x @ yielding) = requires_unyielding x
+                                                ^
+Error: This value is "yielding" but expected to be "unyielding".
+|}]
+
+let f4 (x @ local unyielding) = exclave_ requires_unyielding x
+[%%expect{|
+val f4 : local_ 'a @ unyielding -> local_ unit = <fun>
+|}]
+
+(* [@local_opt] overrides annotations. *)
+external overridden: ('a[@local_opt]) @ local unyielding -> unit = "%ignore"
+
+let succeeds (x @ local) = overridden x
+[%%expect{|
+external overridden : local_ ('a [@local_opt]) @ unyielding -> unit
+  = "%ignore"
+val succeeds : local_ 'a -> unit = <fun>
+|}]
+
+(* [mod global] implies [mod unyielding] by default. *)
+
+type ('a : value mod global) u1
+
+type ('a : value mod global yielding) u2
+
+type w1 : value mod global yielding
+
+type w2 : value mod global unyielding
+
+[%%expect{|
+type ('a : value mod global) u1
+type ('a : value mod global yielding) u2
+type w1 : value mod global yielding
+type w2 : value mod global
+|}]
+
+type _z1 = w1 u1
+
+[%%expect{|
+Line 1, characters 11-13:
+1 | type _z1 = w1 u1
+               ^^
+Error: This type "w1" should be an instance of type "('a : value mod global)"
+       The kind of w1 is value mod global yielding
+         because of the definition of w1 at line 5, characters 0-35.
+       But the kind of w1 must be a subkind of value mod global
+         because of the definition of u1 at line 1, characters 0-31.
+|}]
+
+type _z2 = w2 u1
+
+[%%expect{|
+type _z2 = w2 u1
+|}]
+
+type _z3 = w1 u2
+
+[%%expect{|
+type _z3 = w1 u2
+|}]
+
+type _z4 = w2 u2
+
+[%%expect{|
+type _z4 = w2 u2
+|}]
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 51223c919a6..5c13de8551e 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1662,22 +1662,41 @@ let instance_label ~fixed lbl =
     (vars, ty_arg, ty_res)
   )
 
-let prim_mode mvar = function
-  | Primitive.Prim_global, _ -> Locality.allow_right Locality.global
-  | Primitive.Prim_local, _ -> Locality.allow_right Locality.local
+(* CR dkalinichenko: we must vary yieldingness together with locality to get
+   sane behavior around [@local_opt]. Remove once we have mode polymorphism. *)
+let prim_mode' mvars = function
+  | Primitive.Prim_global, _ ->
+    Locality.allow_right Locality.global, None
+  | Primitive.Prim_local, _ ->
+    Locality.allow_right Locality.local, None
   | Primitive.Prim_poly, _ ->
-    match mvar with
-    | Some mvar -> mvar
+    match mvars with
+    | Some (mvar_l, mvar_y) -> mvar_l, Some mvar_y
     | None -> assert false
 
-(** Returns a new mode variable whose locality is the given locality, while
-    all other axes are from the given [m]. This function is too specific to be
-    put in [mode.ml] *)
-let with_locality locality m =
+(* Exported version. *)
+let prim_mode mvar prim =
+  let mvars = Option.map (fun mvar_l -> mvar_l, Yielding.newvar ()) mvar in
+  fst (prim_mode' mvars prim)
+
+(** Returns a new mode variable whose locality is the given locality and
+    whose yieldingness is the given yieldingness, while all other axes are
+    from the given [m]. This function is too specific to be put in [mode.ml] *)
+let with_locality_and_yielding (locality, yielding) m =
   let m' = Alloc.newvar () in
   Locality.equate_exn (Alloc.proj (Comonadic Areality) m') locality;
-  Alloc.submode_exn m' (Alloc.join_with (Comonadic Areality) Locality.Const.max m);
-  Alloc.submode_exn (Alloc.meet_with (Comonadic Areality) Locality.Const.min m) m';
+  let yielding =
+    Option.value ~default:(Alloc.proj (Comonadic Yielding) m) yielding
+  in
+  Yielding.equate_exn (Alloc.proj (Comonadic Yielding) m') yielding;
+  Alloc.submode_exn m' (Alloc.join_const
+    { Alloc.Const.min with
+      areality = Locality.Const.max;
+      yielding = Yielding.Const.max} m);
+  Alloc.submode_exn (Alloc.meet_const
+    { Alloc.Const.max with
+      areality = Locality.Const.min;
+      yielding = Yielding.Const.min} m) m';
   m'
 
 let curry_mode alloc arg : Alloc.Const.t =
@@ -1701,10 +1720,12 @@ let curry_mode alloc arg : Alloc.Const.t =
     of the return of a function). *)
   {acc with uniqueness=Uniqueness.Const.Aliased}
 
-let rec instance_prim_locals locals mvar macc finalret ty =
+let rec instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ty =
   match locals, get_desc ty with
   | l :: locals, Tarrow ((lbl,marg,mret),arg,ret,commu) ->
-     let marg = with_locality  (prim_mode (Some mvar) l) marg in
+     let marg = with_locality_and_yielding
+      (prim_mode' (Some (mvar_l, mvar_y)) l) marg
+     in
      let macc =
        Alloc.join [
         Alloc.disallow_right mret;
@@ -1714,12 +1735,12 @@ let rec instance_prim_locals locals mvar macc finalret ty =
      in
      let mret =
        match locals with
-       | [] -> with_locality finalret mret
+       | [] -> with_locality_and_yielding (loc, yld) mret
        | _ :: _ ->
           let mret', _ = Alloc.newvar_above macc in (* curried arrow *)
           mret'
      in
-     let ret = instance_prim_locals locals mvar macc finalret ret in
+     let ret = instance_prim_locals locals mvar_l mvar_y macc (loc, yld) ret in
      newty2 ~level:(get_level ty) (Tarrow ((lbl,marg,mret),arg,ret, commu))
   | _ :: _, _ -> assert false
   | [], _ ->
@@ -1796,18 +1817,19 @@ let instance_prim_mode (desc : Primitive.description) ty =
   let is_poly = function Primitive.Prim_poly, _ -> true | _ -> false in
   if is_poly desc.prim_native_repr_res ||
        List.exists is_poly desc.prim_native_repr_args then
-    let mode = Locality.newvar () in
-    let finalret = prim_mode (Some mode) desc.prim_native_repr_res in
+    let mode_l = Locality.newvar () in
+    let mode_y = Yielding.newvar () in
+    let finalret = prim_mode' (Some (mode_l, mode_y)) desc.prim_native_repr_res in
     instance_prim_locals desc.prim_native_repr_args
-      mode (Alloc.disallow_right Alloc.legacy) finalret ty,
-    Some mode
+      mode_l mode_y (Alloc.disallow_right Alloc.legacy) finalret ty,
+    Some mode_l, Some mode_y
   else
-    ty, None
+    ty, None, None
 
 let instance_prim (desc : Primitive.description) ty =
   let ty, sort = instance_prim_layout desc ty in
-  let ty, mode = instance_prim_mode desc ty in
-  ty, mode, sort
+  let ty, mode_l, mode_y = instance_prim_mode desc ty in
+  ty, mode_l, mode_y, sort
 
 (**** Instantiation with parameter substitution ****)
 
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 68908817691..6a821525e54 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -226,7 +226,8 @@ val prim_mode :
         -> (Mode.allowed * 'r) Mode.Locality.t
 val instance_prim:
         Primitive.description -> type_expr ->
-        type_expr * Mode.Locality.lr option * Jkind.Sort.t option
+        type_expr * Mode.Locality.lr option
+        * Mode.Yielding.lr option * Jkind.Sort.t option
 
 (** Given (a @ m1 -> b -> c) @ m0, where [m0] and [m1] are modes expressed by
     user-syntax, [curry_mode m0 m1] gives the mode we implicitly interpret b->c
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 58dee660b85..31a9a417034 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -146,37 +146,31 @@ let value_descriptions ~loc env name
   | Val_prim p1 -> begin
      match vd2.val_kind with
      | Val_prim p2 -> begin
-         let ty1_global, _, _ = Ctype.instance_prim p1 vd1.val_type in
-         let ty2_global =
-           let ty2, mode2, _ = Ctype.instance_prim p2 vd2.val_type in
-           Option.iter
-             (fun m -> Mode.Locality.submode_exn m Mode.Locality.global)
-             mode2;
-           ty2
-         in
-         (try Ctype.moregeneral env true ty1_global ty2_global
-          with Ctype.Moregen err -> raise (Dont_match (Type err)));
-         let ty1_local, _, _ = Ctype.instance_prim p1 vd1.val_type in
-         let ty2_local =
-           let ty2, mode2, _ = Ctype.instance_prim p2 vd2.val_type in
-           Option.iter
-             (fun m -> Mode.Locality.submode_exn Mode.Locality.local m)
-             mode2;
-           ty2
-         in
-         (try Ctype.moregeneral env true ty1_local ty2_local
-          with Ctype.Moregen err -> raise (Dont_match (Type err)));
+         let locality = [ Mode.Locality.global; Mode.Locality.local ] in
+         let yielding = [ Mode.Yielding.unyielding; Mode.Yielding.yielding ] in
+         List.iter (fun loc ->
+           List.iter (fun yield ->
+             let ty1, _, _, _ = Ctype.instance_prim p1 vd1.val_type in
+             let ty2, mode_l2, mode_y2, _ = Ctype.instance_prim p2 vd2.val_type in
+             Option.iter (Mode.Locality.equate_exn loc) mode_l2;
+             Option.iter (Mode.Yielding.equate_exn yield) mode_y2;
+             try 
+               Ctype.moregeneral env true ty1 ty2
+             with Ctype.Moregen err -> 
+               raise (Dont_match (Type err))
+           ) yielding
+         ) locality;
          match primitive_descriptions p1 p2 with
          | None -> Tcoerce_none
          | Some err -> raise (Dont_match (Primitive_mismatch err))
        end
      | _ ->
-        let ty1, mode1, sort1 = Ctype.instance_prim p1 vd1.val_type in
+        let ty1, mode_l1, _, sort1 = Ctype.instance_prim p1 vd1.val_type in
         (try Ctype.moregeneral env true ty1 vd2.val_type
          with Ctype.Moregen err -> raise (Dont_match (Type err)));
         let pc =
           {pc_desc = p1; pc_type = vd2.Types.val_type;
-           pc_poly_mode = Option.map Mode.Locality.disallow_right mode1;
+           pc_poly_mode = Option.map Mode.Locality.disallow_right mode_l1;
            pc_poly_sort=sort1;
            pc_env = env; pc_loc = vd1.Types.val_loc; } in
         Tcoerce_primitive pc
diff --git a/typing/jkind.ml b/typing/jkind.ml
index 219f02e429a..bc12f3a8807 100644
--- a/typing/jkind.ml
+++ b/typing/jkind.ml
@@ -1441,6 +1441,18 @@ module Const = struct
              | acc, `Valid None -> acc
              | Some acc, `Valid (Some mode) -> Some (mode :: acc))
            (Some [])
+      |> function
+      | None -> None
+      | Some modes -> (
+        match List.mem "global" modes, List.mem "unyielding" modes with
+        | true, true ->
+          (* We default [mod global] to [mod global unyielding],
+             so we don't want to print the latter. *)
+          Some (List.filter (fun m -> m <> "unyielding") modes)
+        | true, false ->
+          (* Otherwise, print [mod global yielding] to indicate [yielding]. *)
+          Some (modes @ ["yielding"])
+        | _, _ -> Some modes)
 
     let modality_to_ignore_axes axes_to_ignore =
       (* The modality is constant along axes to ignore and id along others *)
diff --git a/typing/mode.ml b/typing/mode.ml
index 6c790605bfc..28de5e8e31e 100644
--- a/typing/mode.ml
+++ b/typing/mode.ml
@@ -1715,9 +1715,16 @@ module Yielding = struct
 
   include Common (Obj)
 
+  let yielding = of_const Yielding
+
+  let unyielding = of_const Unyielding
+
   let legacy = of_const Const.legacy
 
-  let zap_to_legacy = zap_to_floor
+  (* [unyielding] is the default for [global]s and [yielding] for [local]
+     or [regional] values, so we vary [zap_to_legacy] accordingly. *)
+  let zap_to_legacy ~global =
+    match global with true -> zap_to_floor | false -> zap_to_ceil
 end
 
 let regional_to_local m =
@@ -1806,7 +1813,8 @@ module Comonadic_with (Areality : Areality) = struct
     let areality = proj Areality m |> Areality.zap_to_legacy in
     let linearity = proj Linearity m |> Linearity.zap_to_legacy in
     let portability = proj Portability m |> Portability.zap_to_legacy in
-    let yielding = proj Yielding m |> Yielding.zap_to_legacy in
+    let global = Areality.Const.(equal areality legacy) in
+    let yielding = proj Yielding m |> Yielding.zap_to_legacy ~global in
     { areality; linearity; portability; yielding }
 
   let imply c m =
@@ -2420,18 +2428,18 @@ module Value_with (Areality : Areality) = struct
     let monadic = Monadic.meet_const c.monadic monadic in
     { monadic; comonadic }
 
-  let imply c { comonadic; monadic } =
-    let c = split c in
-    let comonadic = Comonadic.imply c.comonadic comonadic in
-    let monadic = Monadic.imply c.monadic monadic in
-    { monadic; comonadic }
-
   let join_const c { comonadic; monadic } =
     let c = split c in
     let comonadic = Comonadic.join_const c.comonadic comonadic in
     let monadic = Monadic.join_const c.monadic monadic in
     { monadic; comonadic }
 
+  let imply c { comonadic; monadic } =
+    let c = split c in
+    let comonadic = Comonadic.imply c.comonadic comonadic in
+    let monadic = Monadic.imply c.monadic monadic in
+    { monadic; comonadic }
+
   let subtract c { comonadic; monadic } =
     let c = split c in
     let comonadic = Comonadic.subtract c.comonadic comonadic in
diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli
index 8016e8b63b1..f549bec72e7 100644
--- a/typing/mode_intf.mli
+++ b/typing/mode_intf.mli
@@ -287,6 +287,10 @@ module type S = sig
         with module Const := Const
          and type error := error
          and type 'd t = (Const.t, 'd) mode_comonadic
+
+    val yielding : lr
+
+    val unyielding : lr
   end
 
   type 'a comonadic_with =
@@ -471,10 +475,10 @@ module type S = sig
 
     val meet_const : Const.t -> ('l * 'r) t -> ('l * 'r) t
 
-    val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t
-
     val join_const : Const.t -> ('l * 'r) t -> ('l * 'r) t
 
+    val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t
+
     val subtract : Const.t -> ('l * 'r) t -> ('l * disallowed) t
 
     (* The following two are about the scenario where we partially apply a
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index e28083ce475..4242791523c 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -1422,8 +1422,14 @@ Raise if not found. *)
 let tree_of_mode (mode : 'm option) (l : ('m * out_mode) list) : out_mode option =
   Option.map (fun x -> List.assoc x l) mode
 
-let tree_of_modes modes =
+let tree_of_modes (modes : Mode.Alloc.Const.t) =
   let diff = Mode.Alloc.Const.diff modes Mode.Alloc.Const.legacy in
+  (* [yielding] has custom defaults depending on [areality]: *)
+  let diff_yielding =
+    match modes.areality, modes.yielding with
+    | Local, Yielding | Global, Unyielding -> None
+    | _, _ -> Some modes.yielding
+  in
   (* The mapping passed to [tree_of_mode] must cover all non-legacy modes *)
   let l = [
     tree_of_mode diff.areality [Mode.Locality.Const.Local, Omd_legacy Omd_local];
@@ -1432,7 +1438,8 @@ let tree_of_modes modes =
     tree_of_mode diff.portability [Mode.Portability.Const.Portable, Omd_new "portable"];
     tree_of_mode diff.contention [Mode.Contention.Const.Contended, Omd_new "contended";
                                   Mode.Contention.Const.Shared, Omd_new "shared"];
-    tree_of_mode diff.yielding [Mode.Yielding.Const.Yielding, Omd_new "yielding"]]
+    tree_of_mode diff_yielding [Mode.Yielding.Const.Yielding, Omd_new "yielding";
+                                Mode.Yielding.Const.Unyielding, Omd_new "unyielding"]]
   in
   List.filter_map Fun.id l
 
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 1478f732c82..1889eeea99e 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -543,7 +543,9 @@ let mode_coerce mode expected_mode =
 
 let mode_lazy expected_mode =
   let expected_mode =
-    mode_coerce (Value.max_with (Comonadic Areality) Regionality.global)
+    mode_coerce (
+      Value.max_with (Comonadic Areality) Regionality.global
+      |> Value.meet_with (Comonadic Yielding) Yielding.Const.Unyielding)
       expected_mode
   in
   let closure_mode =
@@ -652,6 +654,7 @@ let tuple_pat_mode mode tuple_modes =
 let global_pat_mode {mode; _}=
   let mode =
     Value.meet_with (Comonadic Areality) Regionality.Const.Global mode
+    |> Value.meet_with (Comonadic Yielding) Yielding.Const.Unyielding
   in
   simple_pat_mode mode
 
@@ -6831,13 +6834,19 @@ and type_expect_
         mk_expected (newvar (Jkind.Builtin.value ~why:Boxed_record))
       in
       let exp1 = type_expect ~recarg env (mode_default cell_mode) exp1 cell_type in
-      let exp2 =
+      let new_fields_mode =
         (* The newly-written fields have to be global to avoid heap-to-stack pointers.
            We enforce that here, by asking the allocation to be global.
            This makes the block alloc_heap, but we ignore that information anyway. *)
+        (* CR uniqueness: this shouldn't mention yielding *)
+        { Value.Const.max with
+          areality = Regionality.Const.Global
+        ; yielding = Yielding.Const.Unyielding }
+      in
+      let exp2 =
         let exp2_mode =
           mode_coerce
-            (Value.max_with (Comonadic Areality) Regionality.global)
+            (Value.(meet_const new_fields_mode max |> disallow_left))
             expected_mode
         in
         (* When typing holes, we will enforce: fields_mode <= expected_mode.
@@ -6848,7 +6857,7 @@ and type_expect_
            And we have also checked above that for regionality cell_mode <= expected_mode.
            Therefore, we can safely ignore regionality when checking the mode of holes. *)
         let fields_mode =
-          Value.meet_with (Comonadic Areality) Regionality.Const.Global cell_mode
+          Value.meet_const new_fields_mode cell_mode
             |> Value.disallow_right
         in
         let overwrite =
@@ -7077,7 +7086,7 @@ and type_ident env ?(recarg=Rejected) lid =
   let val_type, kind =
     match desc.val_kind with
     | Val_prim prim ->
-       let ty, mode, sort = instance_prim prim desc.val_type in
+       let ty, mode, _, sort = instance_prim prim desc.val_type in
        let ty = instance ty in
        begin match prim.prim_native_repr_res, mode with
        (* if the locality of returned value of the primitive is poly
diff --git a/typing/typemode.ml b/typing/typemode.ml
index 617ea9cb6bd..dc5a880b592 100644
--- a/typing/typemode.ml
+++ b/typing/typemode.ml
@@ -153,7 +153,28 @@ let transl_modifier_annots annots =
     Transled_modifiers.set ~axis modifiers_so_far (Some { txt = mode; loc })
   in
   let empty_modifiers = Transled_modifiers.empty in
-  List.fold_left step empty_modifiers annots
+  let modifiers = List.fold_left step empty_modifiers annots in
+  (* Since [yielding] is the default mode in presence of [local],
+     the [global] modifier must also apply [unyielding] unless specified. *)
+  match
+    ( Transled_modifiers.get ~axis:(Modal (Comonadic Yielding)) modifiers,
+      Transled_modifiers.get ~axis:(Modal (Comonadic Areality)) modifiers )
+  with
+  | None, Some { txt = Locality.Const.Global; _ } ->
+    Transled_modifiers.set ~axis:(Modal (Comonadic Yielding)) modifiers
+      (Some { txt = Yielding.Const.Unyielding; loc = Location.none })
+  | _, _ -> modifiers
+
+let default_mode_annots (annots : Alloc.Const.Option.t) =
+  (* Unlike all other modes, [yielding] has a different default
+     depending on whether [areality] is [Global] or [Local]. *)
+  let yielding =
+    match annots.yielding, annots.areality with
+    | (Some _ as y), _ | y, None -> y
+    | None, Some Locality.Const.Global -> Some Yielding.Const.Unyielding
+    | None, Some Locality.Const.Local -> Some Yielding.Const.Yielding
+  in
+  { annots with yielding }
 
 let transl_mode_annots annots : Alloc.Const.Option.t =
   let step modifiers_so_far annot =
@@ -172,13 +193,14 @@ let transl_mode_annots annots : Alloc.Const.Option.t =
   in
   let empty_modifiers = Transled_modifiers.empty in
   let modes = List.fold_left step empty_modifiers annots in
-  { areality = Option.map get_txt modes.locality;
-    linearity = Option.map get_txt modes.linearity;
-    uniqueness = Option.map get_txt modes.uniqueness;
-    portability = Option.map get_txt modes.portability;
-    contention = Option.map get_txt modes.contention;
-    yielding = Option.map get_txt modes.yielding
-  }
+  default_mode_annots
+    { areality = Option.map get_txt modes.locality;
+      linearity = Option.map get_txt modes.linearity;
+      uniqueness = Option.map get_txt modes.uniqueness;
+      portability = Option.map get_txt modes.portability;
+      contention = Option.map get_txt modes.contention;
+      yielding = Option.map get_txt modes.yielding
+    }
 
 let untransl_mode_annots ~loc (modes : Mode.Alloc.Const.Option.t) =
   let print_to_string_opt print a = Option.map (Format.asprintf "%a" print) a in
@@ -195,7 +217,15 @@ let untransl_mode_annots ~loc (modes : Mode.Alloc.Const.Option.t) =
   let contention =
     print_to_string_opt Mode.Contention.Const.print modes.contention
   in
-  let yielding = print_to_string_opt Mode.Yielding.Const.print modes.yielding in
+  let yielding =
+    (* Since [yielding] has non-standard defaults, we special-case
+       whether we want to print it here. *)
+    match modes.yielding, modes.areality with
+    | Some Yielding.Const.Yielding, Some Locality.Const.Local
+    | Some Yielding.Const.Unyielding, Some Locality.Const.Global ->
+      None
+    | _, _ -> print_to_string_opt Mode.Yielding.Const.print modes.yielding
+  in
   List.filter_map
     (fun x -> Option.map (fun s -> { txt = Parsetree.Mode s; loc }) x)
     [areality; uniqueness; linearity; portability; contention; yielding]
@@ -269,9 +299,37 @@ let mutable_implied_modalities (mut : Types.mutability) attrs =
     then monadic
     else monadic @ comonadic
 
+(* Since [yielding] is the default mode in presence of [local],
+   the [global] modality must also apply [unyielding] unless specified. *)
+let default_modalities (modalities : Modality.t list) =
+  let areality =
+    List.find_map
+      (function
+        | Modality.Atom (Comonadic Areality, Meet_with a) ->
+          Some (a : Regionality.Const.t)
+        | _ -> None)
+      modalities
+  in
+  let yielding =
+    List.find_map
+      (function
+        | Modality.Atom (Comonadic Yielding, Meet_with y) ->
+          Some (y : Yielding.Const.t)
+        | _ -> None)
+      modalities
+  in
+  let extra =
+    match areality, yielding with
+    | Some Global, None ->
+      [Modality.Atom (Comonadic Yielding, Meet_with Yielding.Const.Unyielding)]
+    | _, _ -> []
+  in
+  modalities @ extra
+
 let transl_modalities ~maturity mut attrs modalities =
   let mut_modalities = mutable_implied_modalities mut attrs in
   let modalities = List.map (transl_modality ~maturity) modalities in
+  let modalities = default_modalities modalities in
   (* mut_modalities is applied before explicit modalities *)
   Modality.Value.Const.id
   |> List.fold_right
@@ -285,9 +343,39 @@ let transl_modalities ~maturity mut attrs modalities =
        (fun atom m -> Modality.Value.Const.compose ~then_:atom m)
        modalities
 
+let untransl_yielding l =
+  let areality =
+    List.find_map
+      (function
+        | Modality.Atom (Comonadic Areality, Meet_with a) ->
+          Some (a : Regionality.Const.t)
+        | _ -> None)
+      l
+  in
+  let yielding =
+    List.find_map
+      (function
+        | Modality.Atom (Comonadic Yielding, Meet_with y) ->
+          Some (y : Yielding.Const.t)
+        | _ -> None)
+      l
+  in
+  match areality, yielding with
+  | Some Global, Some Unyielding | Some Local, Some Yielding -> None
+  | _, Some yld -> Some (Modality.Atom (Comonadic Yielding, Meet_with yld))
+  | _, None -> None
+
 let untransl_modalities mut attrs t =
   let l = Modality.Value.Const.to_list t in
-  let l = List.filter (fun a -> not @@ Modality.is_id a) l in
+  let l =
+    (* [filter_map] instead of [filter] + [append] to preserve order. *)
+    List.filter_map
+      (function
+        | Modality.Atom (Comonadic Yielding, _) -> untransl_yielding l
+        | a when Modality.is_id a -> None
+        | a -> Some a)
+      l
+  in
   let mut_modalities = mutable_implied_modalities mut attrs in
   (* polymorphic equality suffices for now. *)
   let l = List.filter (fun x -> not @@ List.mem x mut_modalities) l in