mode_alpha controls val_modalities

ocaml/testsuite/tests/formatting/test_locations.dlocations.ocamlc.reference

@@ -88,7 +88,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2))
       <def_rec>
         pattern (test_locations.ml[17,534+8]..test_locations.ml[17,534+11])
           Tpat_var "fib"
-          value_mode global,many,nonportable;unique,uncontended
+          value_mode global,many,nonportable;join(shared,contended)(modevar#1[shared,uncontended ... unique,uncontended])
         expression (test_locations.ml[17,534+14]..test_locations.ml[19,572+34])
           Texp_function
           region true

ocaml/testsuite/tests/formatting/test_locations.dno-locations.ocamlc.reference

@@ -88,7 +88,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2))
       <def_rec>
         pattern 
           Tpat_var "fib"
-          value_mode global,many,nonportable;unique,uncontended
+          value_mode global,many,nonportable;join(shared,contended)(modevar#1[shared,uncontended ... unique,uncontended])
         expression 
           Texp_function
           region true

ocaml/testsuite/tests/templates/basic/bad_arg_impl.reference

@@ -2,7 +2,7 @@ File "bad_arg_impl.ml", line 1:
 Error: The argument module bad_arg_impl.ml
        does not match the parameter signature monoid.cmi: 
        Values do not match:
-         val append : unit -> unit -> [> `Banana ] @@ global many portable
+         val append : unit -> unit -> [> `Banana ]
        is not included in
          val append : t -> t -> t
        The type unit -> unit -> [> `Banana ] is not compatible with the type

ocaml/testsuite/tests/typing-modes/modes.ml

@@ -396,3 +396,14 @@ Line 2, characters 43-46:
                                                ^^^
 Error: Modality on primitive is not supported yet.
 |}]
+
+(* modalities on normal values requires [-extension mode_alpha] *)
+module type S = sig
+  val x : string -> string @ local @@ foo bar
+end
+[%%expect{|
+Line 2, characters 38-41:
+2 |   val x : string -> string @ local @@ foo bar
+                                          ^^^
+Error: The extension "mode" is disabled and cannot be used
+|}]

ocaml/testsuite/tests/typing-modes/val_modalities.ml

@@ -1,26 +1,30 @@
 (* TEST
- flags = "-extension unique";
+ flags = "-extension unique -extension mode_alpha";
  expect;
 *)
 
 type r = {
   mutable x : string;
 }
 
+(* In below, printing always gives the strongest modalities possible. Printing
+   backtracks the "zapping to strongest" mutation, so the mutation doesn't
+   persist. *)
+
 let uncontended_use (_ @ uncontended) = ()
 [%%expect{|
 type r = { mutable x : string; }
-val uncontended_use : 'a -> unit = <fun>
+val uncontended_use : 'a -> unit @@ global many = <fun>
 |}]
 
 let share_use : 'a -> unit @@ portable = fun _ -> ()
 [%%expect{|
-val share_use : 'a -> unit = <fun>
+val share_use : 'a -> unit @@ global many = <fun>
 |}]
 
 let (portable_use @ portable) (_ @ portable) = ()
 [%%expect{|
-val portable_use : 'a @ portable -> unit = <fun>
+val portable_use : 'a @ portable -> unit @@ global many = <fun>
 |}]
 
 (* The compiler building itself is a comprehensive test of legacy modules/values.
@@ -30,7 +34,7 @@ module M = struct
   let foo = {x = "hello"}
 end
 [%%expect{|
-module M : sig val foo : r end
+module M : sig val foo : r @@ global many end
 |}]
 
 module type S = sig
@@ -58,15 +62,12 @@ module M = struct
     let x @ contended = "hello"
 end
 [%%expect{|
-module M : sig val x : string @@ contended end
+module M : sig val x : string @@ global many portable contended end
 |}]
 
 (* Testing the defaulting behaviour.
-    "module type of", printing share the same logic. Below, we will only test
-    "module type of".
-
-    Note that the defaulting will mutate the original module type, but printing
-    will backtrack the mutation after the printing is finished.
+   "module type of" triggers the defaulting logic.
+    Note that the defaulting will mutate the original module type.
 *)
 module Module_type_of_comonadic = struct
     module M = struct
@@ -105,11 +106,11 @@ Lines 8-10, characters 35-7:
 10 |     end
 Error: Signature mismatch:
        Modules do not match:
-         sig val x : string @@ contended end
+         sig val x : string @@ global many portable contended end
        is not included in
          sig val x : string end
        Values do not match:
-         val x : string @@ contended
+         val x : string @@ global many portable contended
        is not included in
          val x : string
        The second is empty and the first is contended.
@@ -140,8 +141,9 @@ Lines 8-13, characters 35-7:
 Error: Signature mismatch:
        Modules do not match:
          sig
-           val x : string
-           module N : sig val y : string @@ contended end
+           val x : string @@ global many portable
+           module N :
+             sig val y : string @@ global many portable contended end
          end
        is not included in
          sig
@@ -150,12 +152,12 @@ Error: Signature mismatch:
          end
        In module N:
        Modules do not match:
-         sig val y : string @@ contended end
+         sig val y : string @@ global many portable contended end
        is not included in
          sig val y : string end
        In module N:
        Values do not match:
-         val y : string @@ contended
+         val y : string @@ global many portable contended
        is not included in
          val y : string
        The second is empty and the first is contended.
@@ -173,7 +175,8 @@ module Without_inclusion = struct
     let () = portable_use M.x
 end
 [%%expect{|
-module Without_inclusion : sig module M : sig val x : string end end
+module Without_inclusion :
+  sig module M : sig val x : string @@ global many portable end end
 |}]
 
 module Without_inclusion = struct
@@ -203,11 +206,11 @@ Lines 4-6, characters 10-7:
 6 |     end
 Error: Signature mismatch:
        Modules do not match:
-         sig val x : string @@ contended end
+         sig val x : string @@ global many portable contended end
        is not included in
          sig val x : string end
        Values do not match:
-         val x : string @@ contended
+         val x : string @@ global many portable contended
        is not included in
          val x : string
        The second is empty and the first is contended.
@@ -266,7 +269,10 @@ module Close_over_value = struct
 end
 [%%expect{|
 module Close_over_value :
-  sig module M : sig val x : string end val foo : unit -> unit end
+  sig
+    module M : sig val x : string @@ global many portable end
+    val foo : unit -> unit @@ global many portable
+  end
 |}]
 
 module Close_over_value_monadic = struct

ocaml/testsuite/tests/typing-modes/val_modalities_floor.ml

@@ -9,6 +9,7 @@ strongest instead of legacy *)
  ";
 {
    setup-ocamlopt.byte-build-env;
+   flags = "-extension mode_alpha";
 
    {
     src = "def_portable.ml";

ocaml/testsuite/tests/typing-private/private.compilers.principal.reference

@@ -75,7 +75,10 @@ Line 3, characters 2-51:
 3 |   struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
-       ...
+       Modules do not match:
+         sig type t = int val f : int -> t end
+       is not included in
+         sig type t = private Foobar.t val f : int -> t end
        Type declarations do not match:
          type t = int
        is not included in

ocaml/testsuite/tests/typing-private/private.compilers.reference

@@ -75,7 +75,10 @@ Line 3, characters 2-51:
 3 |   struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: Signature mismatch:
-       ...
+       Modules do not match:
+         sig type t = int val f : int -> t end
+       is not included in
+         sig type t = private Foobar.t val f : int -> t end
        Type declarations do not match:
          type t = int
        is not included in

ocaml/typing/printtyp.ml

@@ -2027,7 +2027,7 @@ let tree_of_value_description id decl =
   (* Important: process the fvs *after* the type; tree_of_type_scheme
      resets the naming context *)
   let snap = Btype.snapshot () in
-  let moda = Mode.Modality.Value.zap_to_id decl.val_modalities in
+  let moda = Mode.Modality.Value.zap_to_floor decl.val_modalities in
   let qtvs = extract_qtvs [decl.val_type] in
   let apparent_arity =
     let rec count n typ =

ocaml/typing/typedecl.ml

@@ -426,7 +426,9 @@ 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 modalities =
+          Typemode.transl_modalities ~maturity:Stable mut 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;
@@ -462,8 +464,13 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc =
 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 cty =
+      transl_simple_type ~new_var_jkind env ?univars ~closed
+        Mode.Alloc.Const.legacy arg.pca_type
+    in
+    let gf =
+      Typemode.transl_modalities ~maturity:Stable Immutable arg.pca_modalities
+    in
     {ca_modalities = gf; ca_type = cty; ca_loc = arg.pca_loc}
   in
   let tyl_gfl = List.map mk cal in
@@ -2875,7 +2882,7 @@ let transl_value_decl env loc valdecl =
     [] when Env.is_in_signature env ->
       let modalities =
         valdecl.pval_modalities
-        |> Typemode.transl_modalities Immutable
+        |> Typemode.transl_modalities ~maturity:Alpha Immutable
         |> Mode.Modality.Value.of_const
       in
       let default_arity =

ocaml/typing/typemod.ml

@@ -98,7 +98,7 @@ type error =
       old_arg_type : Compilation_unit.Name.t option;
       old_source_file : Misc.filepath;
     }
-  | Submode_failed of Mode.Value.Comonadic.error
+  | Submode_failed of Mode.Value.error
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
@@ -2425,6 +2425,31 @@ let simplify_app_summary app_view = match app_view.arg with
     | false, Some p -> Includemod.Error.Named p, mty
     | false, None   -> Includemod.Error.Anonymous, mty
 
+let maybe_infer_modalities ~loc ~env ~md_mode ~mode =
+  if Language_extension.(is_at_least Mode Alpha) then begin
+    (* Upon construction, for comonadic (prescriptive) axes, module
+    must be weaker than the values therein, for otherwise operations
+    would be allowed to performed on the module (and extended to the
+    values) that's disallowed for the values.
+
+    For monadic (descriptive) axes, the restriction is not on the
+    construction but on the projection, which is modelled by the
+    [Diff] modality in [mode.ml]. *)
+    begin match Mode.Value.Comonadic.submode
+      mode.Mode.comonadic
+      md_mode.Mode.comonadic with
+      | Ok () -> ()
+      | Error (Error (ax, e)) -> raise (Error (loc, env, Submode_failed (Error (Comonadic ax, e))))
+    end;
+    Mode.Modality.Value.infer ~md_mode ~mode
+  end else begin
+    begin match Mode.Value.submode mode md_mode with
+      | Ok () -> ()
+      | Error e -> raise (Error (loc, env, Submode_failed e))
+    end;
+    Mode.Modality.Value.id
+  end
+
 let rec type_module ?(alias=false) sttn funct_body anchor env smod =
   Builtin_attributes.warning_scope smod.pmod_attributes
     (fun () -> type_module_aux ~alias sttn funct_body anchor env smod)
@@ -2885,21 +2910,9 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
               Signature_names.check_value names first_loc id;
               let vd, mode =  Env.find_value_no_locks_exn id newenv in
               let vd = Subst.Lazy.force_value_description vd in
-              (* Upon construction, for comonadic (prescriptive) axes, module
-              must be weaker than the values therein, for otherwise operations
-              would be allowed to performed on the module (and extended to the
-              values) that's disallowed for the values.
-
-              For monadic (descriptive) axes, the restriction is not on the
-              construction but on the projection, which is modelled by the
-              [Diff] modality in [mode.ml]. *)
-              begin match Mode.Value.Comonadic.submode
-                mode.Mode.comonadic
-                md_mode.Mode.comonadic with
-                | Ok () -> ()
-                | Error e -> raise (Error (first_loc, env, Submode_failed e))
-              end;
-              let modalities = Mode.Modality.Value.infer ~md_mode ~mode in
+              let modalities =
+                maybe_infer_modalities ~loc:first_loc ~env ~md_mode ~mode
+              in
               let vd =
                 { vd with
                   val_zero_alloc = zero_alloc;
@@ -4073,8 +4086,8 @@ let report_error ~loc _env = function
   | Submode_failed (Error (ax, {left; right})) ->
       Location.errorf ~loc
         "This value is %a, but expected to be %a because it is inside a module."
-        (Mode.Value.Comonadic.Const.print_axis ax) left
-        (Mode.Value.Comonadic.Const.print_axis ax) right
+        (Mode.Value.Const.print_axis ax) left
+        (Mode.Value.Const.print_axis ax) right
 
 let report_error env ~loc err =
   Printtyp.wrap_printing_env_error env

ocaml/typing/typemod.mli

@@ -160,7 +160,7 @@ type error =
       old_arg_type: Compilation_unit.Name.t option;
       old_source_file: Misc.filepath;
     }
-  | Submode_failed of Mode.Value.Comonadic.error
+  | Submode_failed of Mode.Value.error
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error

ocaml/typing/typemode.ml

@@ -14,7 +14,8 @@ let transl_mode_annots modes =
     | [] -> acc
     | m :: rest ->
       let { txt; loc } = (m : Mode_expr.Const.t :> _ Location.loc) in
-      Jane_syntax_parsing.assert_extension_enabled ~loc Mode ();
+      Jane_syntax_parsing.assert_extension_enabled ~loc Mode
+        Language_extension.Stable;
       let acc : Alloc.Const.Option.t =
         match txt with
         (* CR zqian: We should interpret other mode names (global, shared, once)
@@ -53,10 +54,10 @@ let transl_mode_annots modes =
   in
   loop Alloc.Const.Option.none modes.txt
 
-let transl_modality m : Modality.t =
+let transl_modality ~maturity m : Modality.t =
   let { txt; loc } = m in
   let (Parsetree.Modality s) = txt in
-  Jane_syntax_parsing.assert_extension_enabled ~loc Mode ();
+  Jane_syntax_parsing.assert_extension_enabled ~loc Mode maturity;
   match s with
   | "global" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Global)
   | "local" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Local)
@@ -117,8 +118,8 @@ let is_mutable_implied_modality m =
   (* polymorphic equality suffices for now. *)
   List.mem m mutable_implied_modalities
 
-let transl_modalities mut modalities =
-  let modalities = List.map transl_modality modalities in
+let transl_modalities ~maturity mut modalities =
+  let modalities = List.map (transl_modality ~maturity) modalities in
   let modalities =
     if Types.is_mutable mut
     then modalities @ mutable_implied_modalities

ocaml/typing/typemode.mli

@@ -5,8 +5,10 @@ val transl_mode_annots : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.Option.t
     legacy if unspecified *)
 val transl_alloc_mode : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.t
 
-(** Interpret mode syntax as modalities *)
+(** Interpret mode syntax as modalities. Modalities occuring at different places
+    requires different levels of maturity. *)
 val transl_modalities :
+  maturity:Language_extension.maturity ->
   Types.mutability ->
   Parsetree.modality Location.loc list ->
   Mode.Modality.Value.Const.t