Remove @no_mutable_implied_modalities

parsing/builtin_attributes.ml

@@ -113,7 +113,6 @@ let builtin_attrs =
   ; "only_generative_effects"
   ; "error_message"
   ; "layout_poly"
-  ; "no_mutable_implied_modalities"
   ; "or_null_reexport"
   ; "no_recursive_modalities"
   ; "jane.non_erasable.instances"
@@ -650,9 +649,6 @@ let parse_standard_implementation_attributes attr =
   zero_alloc_attribute ~in_signature:false attr;
   unsafe_allow_any_mode_crossing_attribute attr
 
-let has_no_mutable_implied_modalities attrs =
-  has_attribute "no_mutable_implied_modalities" attrs
-
 let has_local_opt attrs =
   has_attribute "local_opt" attrs
 

parsing/builtin_attributes.mli

@@ -212,7 +212,6 @@ val parse_standard_implementation_attributes : Parsetree.attribute -> unit
 val curry_attr_name : string
 val curry_attr : Location.t -> Parsetree.attribute
 
-val has_no_mutable_implied_modalities: Parsetree.attributes -> bool
 val has_local_opt: Parsetree.attributes -> bool
 val has_layout_poly: Parsetree.attributes -> bool
 val has_curry: Parsetree.attributes -> bool

testsuite/tests/parsetree/source_jane_street.ml

@@ -601,8 +601,8 @@ type t = { x : string @@ global
 type t1 = { mutable x : float
           ; mutable f : float -> float }
 
-type t2 = { mutable x : float [@no_mutable_implied_modalities]
-          ; mutable f : float -> float [@no_mutable_implied_modalities] }
+type t2 = { mutable x : float @@ local once
+          ; mutable f : float -> float @@ local once }
 
 [%%expect{|
 type t =
@@ -614,7 +614,10 @@ type t = {
   z : string @@ global many;
 }
 type t1 = { mutable x : float; mutable f : float -> float; }
-type t2 = { mutable x : float; mutable f : float -> float; }
+type t2 = {
+  mutable x : float @@ local once;
+  mutable f : float -> float @@ local once;
+}
 |}]
 
 let f1 (x @ local) (f @ once) : t1 = exclave_ { x; f }

testsuite/tests/typing-jkind-bounds/basics.ml

@@ -1157,7 +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 {|
-type 'a t = { x : 'a @@ global many portable aliased contended; } [@@unboxed]
+type 'a t = { x : 'a @@ global many aliased portable 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

testsuite/tests/typing-layouts/allow_any.ml

@@ -385,9 +385,9 @@ Lines 1-2, characters 0-34:
 Error: This variant or record definition does not match that of type "'a t"
        They have different unsafe mode crossing behavior:
        Both specify [@@unsafe_allow_any_mode_crossing], but their bounds are not equal
-         the original has: mod many portable unyielding stateless contended
+         the original has: mod many portable contended unyielding stateless
          immutable with 'a
-         but this has: mod many portable unyielding stateless contended
+         but this has: mod many portable contended unyielding stateless
          immutable
 |}]
 
@@ -406,9 +406,9 @@ Error: This variant or record definition does not match that of type
          "('a, 'b) arity_2"
        They have different unsafe mode crossing behavior:
        Both specify [@@unsafe_allow_any_mode_crossing], but their bounds are not equal
-         the original has: mod many portable unyielding stateless contended
+         the original has: mod many portable contended unyielding stateless
          immutable with 'b
-         but this has: mod many portable unyielding stateless contended
+         but this has: mod many portable contended unyielding stateless
          immutable with 'a
 |}]
 

testsuite/tests/typing-modes/mutable.ml

@@ -16,14 +16,57 @@ Line 2, characters 31-32:
 Error: This value escapes its region.
 |}]
 
-(* [@no_mutable_implied_modalities] disables those implied modalities on the
-   comonadic axes, and allows us to test [mutable] alone *)
+(* you can override those implied modalities *)
+type r = {mutable s : string @@ local}
+let foo (local_ s) = exclave_ {s}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+val foo : local_ string -> local_ r = <fun>
+|}]
+
+type r = {mutable s : string @@ global}
+[%%expect{|
+type r = { mutable s : string; }
+|}]
+
+type r = {mutable s : string @@ global yielding}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ yielding global}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ yielding}
+[%%expect{|
+type r = { mutable s : string @@ yielding; }
+|}]
+
+type r = {mutable s : string @@ local yielding}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+|}]
+
+type r = {mutable s : string @@ yielding local}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+|}]
 
-(* Note the attribute is not printed back, which might be confusing.
-   Considering this is a short-term workaround, let's not worry too much. *)
-type 'a r = {mutable s : 'a [@no_mutable_implied_modalities]}
+type r = {mutable s : string @@ local unyielding}
 [%%expect{|
-type 'a r = { mutable s : 'a; }
+type r = { mutable s : string @@ local; }
+|}]
+
+type r = {mutable s : string @@ unyielding local}
+[%%expect{|
+type r = { mutable s : string @@ local; }
+|}]
+
+type 'a r = {mutable s : 'a @@ local}
+[%%expect{|
+type 'a r = { mutable s : 'a @@ local; }
 |}]
 
 (* We can now construct a local record using a local field. *)
@@ -56,11 +99,11 @@ let foo (local_ r) =
 val foo : local_ string r -> unit = <fun>
 |}]
 
-(* We can still add modalities explicitly. Of course, the print-back is
-   confusing. *)
-type r' = {mutable s' : string @@ global [@no_mutable_implied_modalities]}
+(* We can still add modalities explicitly. But they might be omitted if they are
+  the same as the mutable-implied ones. *)
+type r' = {mutable s' : string @@ global}
 [%%expect{|
-type r' = { mutable global_ s' : string; }
+type r' = { mutable s' : string; }
 |}]
 
 let foo (local_ s') = exclave_ {s'}
@@ -104,7 +147,7 @@ Error: This value is "aliased" but expected to be "unique".
 |}]
 
 module M : sig
-  type t = { mutable s : string [@no_mutable_implied_modalities] }
+  type t = { mutable s : string @@ local }
 end = struct
   type t = { mutable s : string }
 end
@@ -117,39 +160,39 @@ Error: Signature mismatch:
        Modules do not match:
          sig type t = { mutable s : string; } end
        is not included in
-         sig type t = { mutable s : string; } end
+         sig type t = { mutable s : string @@ local; } end
        Type declarations do not match:
          type t = { mutable s : string; }
        is not included in
-         type t = { mutable s : string; }
+         type t = { mutable s : string @@ local; }
        Fields do not match:
          "mutable s : string;"
        is not the same as:
-         "mutable s : string;"
+         "mutable s : string @@ local;"
        The first is global and the second is not.
 |}]
 
 module M : sig
   type t = { mutable s : string }
 end = struct
-  type t = { mutable s : string [@no_mutable_implied_modalities] }
+  type t = { mutable s : string @@ local}
 end
 [%%expect{|
 Lines 3-5, characters 6-3:
 3 | ......struct
-4 |   type t = { mutable s : string [@no_mutable_implied_modalities] }
+4 |   type t = { mutable s : string @@ local}
 5 | end
 Error: Signature mismatch:
        Modules do not match:
-         sig type t = { mutable s : string; } end
+         sig type t = { mutable s : string @@ local; } end
        is not included in
          sig type t = { mutable s : string; } end
        Type declarations do not match:
-         type t = { mutable s : string; }
+         type t = { mutable s : string @@ local; }
        is not included in
          type t = { mutable s : string; }
        Fields do not match:
-         "mutable s : string;"
+         "mutable s : string @@ local;"
        is not the same as:
          "mutable s : string;"
        The second is global and the first is not.

testsuite/tests/typing-modes/val_modalities.ml

@@ -42,8 +42,7 @@ module type S = sig
       portable nonportable
 end
 [%%expect{|
-module type S =
-  sig val x : string @@ global many portable aliased contended end
+module type S = sig val x : string @@ many aliased contended end
 |}]
 
 (* values' comonadic axes must be lower than the module *)

testsuite/tests/warnings/w53.compilers.reference

@@ -1,8 +1,3 @@
-File "w53.ml", line 9, characters 24-53:
-9 | type r0 = {s : string [@no_mutable_implied_modalities]} (* rejected *)
-                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 53 [misplaced-attribute]: the "no_mutable_implied_modalities" attribute cannot appear in this context
-
 File "w53.ml", line 15, characters 16-21:
 15 |   val x : int [@alert foo "foo"] (* rejected *)
                      ^^^^^

testsuite/tests/warnings/w53.ml

@@ -6,8 +6,8 @@
  check-ocamlc.byte-output;
 *)
 
-type r0 = {s : string [@no_mutable_implied_modalities]} (* rejected *)
-type r1 = {mutable s : string [@no_mutable_implied_modalities]} (* accepted *)
+
+
 
 module type TestAlertSig = sig
   type t1 = Foo1 [@alert foo "foo"] (* accepted *)

typing/jkind.ml

@@ -399,7 +399,7 @@ let relevant_axes_of_modality ~relevant_for_nullability ~modality =
       | Modal axis ->
         let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
         let modality = Mode.Modality.Value.Const.proj axis modality in
-        not (Mode.Modality.is_constant modality)
+        not (Mode.Modality.is_constant (Atom (axis, modality)))
       (* The kind-inference.md document (in the repo) discusses both constant
          modalities and identity modalities. Of course, reality has modalities
          (such as [shared]) that are neither constants nor identities. Here, we
@@ -1209,7 +1209,7 @@ let outcometree_of_type = ref (fun _ -> assert false)
 
 let set_outcometree_of_type p = outcometree_of_type := p
 
-let outcometree_of_modalities_new = ref (fun _ _ _ -> assert false)
+let outcometree_of_modalities_new = ref (fun _ _ -> assert false)
 
 let set_outcometree_of_modalities_new p = outcometree_of_modalities_new := p
 
@@ -1602,7 +1602,7 @@ module Const = struct
         (fun acc (Axis.Pack axis) ->
           match axis with
           | Modal axis ->
-            let then_ : Modality.t =
+            let t : Modality.t =
               let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
               match axis with
               | Monadic monadic ->
@@ -1613,7 +1613,8 @@ module Const = struct
                   ( axis,
                     Meet_with (Mode.Value.Comonadic.Const.min_axis comonadic) )
             in
-            Modality.Value.Const.compose acc ~then_
+            let (Atom (axis, a)) = t in
+            Modality.Value.Const.set axis a acc
           | Nonmodal _ ->
             (* TODO: don't know how to print *)
             acc)
@@ -1637,7 +1638,7 @@ module Const = struct
             in
             ( !outcometree_of_type type_expr,
               !outcometree_of_modalities_new
-                Types.Immutable []
+                Types.Immutable
                 (modality_to_ignore_axes axes_ignored_by_modalities) ))
           (With_bounds.to_list actual.with_bounds)
       in
@@ -1818,7 +1819,7 @@ module Const = struct
       | Left_jkind (transl_type, _) ->
         let type_ = transl_type type_ in
         let modality =
-          Typemode.transl_modalities ~maturity:Stable Immutable [] modalities
+          Typemode.transl_modalities ~maturity:Stable Immutable modalities
         in
         { layout = base.layout;
           mod_bounds = base.mod_bounds;

typing/jkind.mli

@@ -637,7 +637,6 @@ val set_outcometree_of_type : (Types.type_expr -> Outcometree.out_type) -> unit
 
 val set_outcometree_of_modalities_new :
   (Types.mutability ->
-  Parsetree.attributes ->
   Mode.Modality.Value.Const.t ->
   Outcometree.out_mode_new list) ->
   unit