local implies yielding (#3532)

* `local` implies `yielding`

* accept tests

* `yielding` tests

* format

* dirty fix test change

* small improvement

* merge fix

* fix printing bounds

* accept tests

* fix the issue with `instance_prim`

* Only vary `yielding` with `[@local_opt]`

* fixes

* tests

* fix lazy

* format

* keep order

* fix mixed mode annots

* fixes

* fix

* rebase + accept

---------

Co-authored-by: Diana Kalinichenko <[email protected]>
Co-authored-by: Zesen Qian <[email protected]>

Author: 3 people

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 ->

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.

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

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

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; }

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; }
 |}]
 
 (*******************)

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")