flambda-backend: Add [@no_mutable_implied_modalities] (#2716)

Author: riaqn

parsing/builtin_attributes.ml

@@ -109,6 +109,7 @@ let builtin_attrs =
   ; "only_generative_effects"; "ocaml.only_generative_effects"
   ; "error_message"; "ocaml.error_message"
   ; "layout_poly"; "ocaml.layout_poly"
+  ; "no_mutable_implied_modalities"; "ocaml.no_mutable_implied_modalities"
   ]
 
 (* nroberts: When we upstream the builtin-attribute whitelisting, we shouldn't
@@ -634,6 +635,9 @@ let parse_standard_implementation_attributes attr =
   flambda_oclassic_attribute attr;
   zero_alloc_attribute attr
 
+let has_no_mutable_implied_modalities attrs =
+  has_attribute ["ocaml.no_mutable_implied_modalities";"no_mutable_implied_modalities"] attrs
+
 let has_local_opt attrs =
   has_attribute ["ocaml.local_opt"; "local_opt"] attrs
 

parsing/builtin_attributes.mli

@@ -178,6 +178,7 @@ val has_boxed: Parsetree.attributes -> bool
 val parse_standard_interface_attributes : Parsetree.attribute -> unit
 val parse_standard_implementation_attributes : Parsetree.attribute -> unit
 
+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/typing-modes/mutable.ml

@@ -1,14 +1,147 @@
 (* TEST
- flags = "-extension unique";
+ flags = "-extension unique -w +53";
  expect;
 *)
 
 (* This file tests the typing around mutable() logic. *)
 
-(* For legacy compatibility, [mutable] implies [global] [shared] and [many].
-   Therefore, the effect of mutable in isolation is not testable yet. *)
+(* By default, mutable implies [global many shared] modalities *)
+type r = {mutable s : string}
+let foo (local_ s) = local_ {s}
+[%%expect{|
+type r = { mutable s : string; }
+Line 2, characters 29-30:
+2 | let foo (local_ s) = local_ {s}
+                                 ^
+Error: This value escapes its region.
+|}]
+
+(* [@no_mutable_implied_modalities] disables those implied modalities, and
+   allows us to test [mutable] alone *)
+
+(* 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]}
+[%%expect{|
+type 'a r = { mutable s : 'a; }
+|}]
+
+(* We can now construct a local record using a local field. *)
+let foo (local_ s) = local_ {s}
+[%%expect{|
+val foo : local_ 'a -> local_ 'a r = <fun>
+|}]
+
+(* Mutation needs to be global *)
+let foo (local_ r) =
+  r.s <- (local_ "hello")
+[%%expect{|
+Line 2, characters 9-25:
+2 |   r.s <- (local_ "hello")
+             ^^^^^^^^^^^^^^^^
+Error: This value escapes its region.
+|}]
+
+let foo (local_ r) = ref r.s
+[%%expect{|
+Line 1, characters 25-28:
+1 | let foo (local_ r) = ref r.s
+                             ^^^
+Error: This value escapes its region.
+|}]
+
+let foo (local_ r) =
+  r.s <- "hello"
+[%%expect{|
+val foo : local_ string r -> unit = <fun>
+|}]
 
-(* CR zqian: add test for mutable when mutable is decoupled from modalities. *)
+(* We can still add modalities explicitly. Of course, the print-back is
+   confusing. *)
+type r' = {mutable s' : string @@ global [@no_mutable_implied_modalities]}
+[%%expect{|
+type r' = { mutable global_ s' : string; }
+|}]
+
+let foo (local_ s') = local_ {s'}
+[%%expect{|
+Line 1, characters 30-32:
+1 | let foo (local_ s') = local_ {s'}
+                                  ^^
+Error: This value escapes its region.
+|}]
+
+(* mutable defaults to mutable(legacy = nonportable), so currently we can't construct a
+   portable record (ignoring mode-crossing). *)
+let foo (s @ portable) = ({s} : _ @@ portable)
+[%%expect{|
+Line 1, characters 26-29:
+1 | let foo (s @ portable) = ({s} : _ @@ portable)
+                              ^^^
+Error: This value is nonportable but expected to be portable.
+|}]
+
+(* For monadic axes, mutable defaults to mutable(min). So currently we can't
+   write a [contended] value to a mutable field. *)
+let foo (r @ uncontended) (s @ contended) = r.s <- s
+[%%expect{|
+Line 1, characters 51-52:
+1 | let foo (r @ uncontended) (s @ contended) = r.s <- s
+                                                       ^
+Error: This value is contended but expected to be uncontended.
+|}]
+
+module M : sig
+  type t = { mutable s : string [@no_mutable_implied_modalities] }
+end = struct
+  type t = { mutable s : string }
+end
+[%%expect{|
+Lines 3-5, characters 6-3:
+3 | ......struct
+4 |   type t = { mutable s : string }
+5 | end
+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
+       Type declarations do not match:
+         type t = { mutable s : string; }
+       is not included in
+         type t = { mutable s : string; }
+       Fields do not match:
+         mutable s : string;
+       is not the same as:
+         mutable s : string;
+       The second is empty and the first is shared.
+|}]
+
+module M : sig
+  type t = { mutable s : string }
+end = struct
+  type t = { mutable s : string [@no_mutable_implied_modalities] }
+end
+[%%expect{|
+Lines 3-5, characters 6-3:
+3 | ......struct
+4 |   type t = { mutable s : string [@no_mutable_implied_modalities] }
+5 | end
+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
+       Type declarations do not match:
+         type t = { mutable s : string; }
+       is not included in
+         type t = { mutable s : string; }
+       Fields do not match:
+         mutable s : string;
+       is not the same as:
+         mutable s : string;
+       The second is global_ and the first is not.
+|}]
 
 type r =
   { f : string -> string;

testsuite/tests/warnings/w53.compilers.reference

@@ -8,6 +8,11 @@ File "w53.ml", line 12, characters 4-5:
          ^
 Warning 32 [unused-value-declaration]: unused value h.
 
+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 12, characters 14-20:
 12 | let h x = x [@inline] (* rejected *)
                    ^^^^^^

testsuite/tests/warnings/w53.ml

@@ -4,11 +4,11 @@
 
 
 
-
-
-
 *)
 
+type r0 = {s : string [@no_mutable_implied_modalities]} (* rejected *)
+type r1 = {mutable s : string [@no_mutable_implied_modalities]} (* accepted *)
+
 let h x = x [@inline] (* rejected *)
 let h x = x [@ocaml.inline] (* rejected *)
 

typing/printtyp.ml

@@ -1309,11 +1309,11 @@ let tree_of_modality (t : Mode.Modality.t) =
       Some (Ogf_legacy Ogf_global)
   | _ -> Option.map (fun x -> Ogf_new x) (tree_of_modality_new t)
 
-let tree_of_modalities mutability t =
+let tree_of_modalities ~has_mutable_implied_modalities t =
   let l = Mode.Modality.Value.to_list t in
   (* CR zqian: decouple mutable and modalities *)
   let l =
-    if Types.is_mutable mutability then
+    if has_mutable_implied_modalities then
       List.filter (fun m -> not @@ Typemode.is_mutable_implied_modality m) l
     else
       l
@@ -1502,7 +1502,8 @@ and tree_of_labeled_typlist mode tyl =
   List.map (fun (label, ty) -> label, tree_of_typexp mode Alloc.Const.legacy ty) tyl
 
 and tree_of_typ_gf {ca_type=ty; ca_modalities=gf; _} =
-  (tree_of_typexp Type Alloc.Const.legacy ty, tree_of_modalities Immutable gf)
+  (tree_of_typexp Type Alloc.Const.legacy ty,
+   tree_of_modalities ~has_mutable_implied_modalities:false gf)
 
 (** We are on the RHS of an arrow type, where [ty] is the return type, and [m]
     is the return mode. This function decides the printed modes on [ty].
@@ -1689,7 +1690,15 @@ let tree_of_label l =
         mut
     | Immutable -> Om_immutable
   in
-  let ld_modalities = tree_of_modalities l.ld_mutable l.ld_modalities in
+  let has_mutable_implied_modalities =
+    if is_mutable l.ld_mutable then
+      not (Builtin_attributes.has_no_mutable_implied_modalities l.ld_attributes)
+    else
+      false
+  in
+  let ld_modalities =
+    tree_of_modalities ~has_mutable_implied_modalities l.ld_modalities
+  in
   (Ident.name l.ld_id, mut, tree_of_typexp Type l.ld_type, ld_modalities)
 
 let tree_of_constructor_arguments = function

typing/typedecl.ml

@@ -426,7 +426,15 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc =
           | Immutable -> Immutable
           | Mutable -> Mutable Mode.Alloc.Comonadic.Const.legacy
          in
-         let modalities = Typemode.transl_modalities mut modalities in
+         let has_mutable_implied_modalities =
+          if Types.is_mutable mut then
+            not (Builtin_attributes.has_no_mutable_implied_modalities attrs)
+          else
+            false
+         in
+         let modalities =
+          Typemode.transl_modalities ~has_mutable_implied_modalities modalities
+         in
          let arg = Ast_helper.Typ.force_poly arg in
          let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg in
          {ld_id = Ident.create_local name.txt;
@@ -463,7 +471,10 @@ let transl_types_gf ~new_var_jkind ~allow_unboxed
   env loc univars closed cal kloc =
   let mk arg =
     let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg.pca_type in
-    let gf = Typemode.transl_modalities Immutable arg.pca_modalities in
+    let gf =
+      Typemode.transl_modalities ~has_mutable_implied_modalities:false
+        arg.pca_modalities
+    in
     {ca_modalities = gf; ca_type = cty; ca_loc = arg.pca_loc}
   in
   let tyl_gfl = List.map mk cal in

typing/typemode.ml

@@ -115,10 +115,10 @@ let is_mutable_implied_modality m =
   (* polymorphic equality suffices for now. *)
   List.mem m mutable_implied_modalities
 
-let transl_modalities mut modalities =
+let transl_modalities ~has_mutable_implied_modalities modalities =
   let modalities = List.map transl_modality modalities in
   let modalities =
-    if Types.is_mutable mut
+    if has_mutable_implied_modalities
     then modalities @ mutable_implied_modalities
     else modalities
   in

typing/typemode.mli

@@ -7,7 +7,7 @@ val transl_alloc_mode : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.t
 
 (** Interpret mode syntax as modalities *)
 val transl_modalities :
-  Types.mutability ->
+  has_mutable_implied_modalities:bool ->
   Parsetree.modality Location.loc list ->
   Mode.Modality.Value.t