Revert c29a7bb to disable unique mutable fields again

testsuite/tests/typing-modes/modes.ml

@@ -297,7 +297,7 @@ type r = {
   mutable x : string @@ global aliased many
 }
 [%%expect{|
-type r = { mutable x : string @@ aliased; }
+type r = { mutable x : string; }
 |}]
 
 

testsuite/tests/typing-modes/mutable.ml

@@ -75,7 +75,10 @@ Error: This value escapes its region.
    portable record (ignoring mode-crossing). *)
 let foo (s @ portable) = ({s} : _ @@ portable)
 [%%expect{|
-val foo : 'a @ portable -> 'a r = <fun>
+Line 1, characters 26-29:
+1 | let foo (s @ portable) = ({s} : _ @@ portable)
+                              ^^^
+Error: This value is "nonportable" but expected to be "portable".
 |}]
 
 (* This attribute doesn't disable implied modalities on monadic axes. For
@@ -89,15 +92,15 @@ val foo : 'a r -> 'a -> unit = <fun>
 
 let foo (s @ aliased) = ({s} : _ @@ unique)
 [%%expect{|
-Line 1, characters 26-27:
-1 | let foo (s @ aliased) = ({s} : _ @@ unique)
-                              ^
-Error: This value is "aliased" but expected to be "unique".
+val foo : 'a -> 'a r = <fun>
 |}]
 
 let foo (r @ unique) = (r.s : _ @@ unique)
 [%%expect{|
-val foo : 'a r @ unique -> 'a = <fun>
+Line 1, characters 24-27:
+1 | let foo (r @ unique) = (r.s : _ @@ unique)
+                            ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 module M : sig
@@ -161,7 +164,10 @@ let r @ portable =
 (* CR mode-crossing: The [m0] in mutable should cross modes upon construction. *)
 [%%expect{|
 type r = { f : string -> string; mutable a : int; }
-val r : r = {f = <fun>; a = 42}
+Lines 5-6, characters 2-12:
+5 | ..{ f = (fun x -> x);
+6 |     a = 42 }
+Error: This value is "nonportable" but expected to be "portable".
 |}]
 
 type r =
@@ -174,5 +180,8 @@ let r @ portable =
    in modality; as a result, it enjoys mode crossing enabled by the modality. *)
 [%%expect{|
 type r = { f : string -> string; mutable g : string -> string @@ portable; }
-val r : r = {f = <fun>; g = <fun>}
+Lines 5-6, characters 2-20:
+5 | ..{ f = (fun x -> x);
+6 |     g = fun x -> x }
+Error: This value is "nonportable" but expected to be "portable".
 |}]

testsuite/tests/typing-modes/portable-contend.ml

@@ -166,7 +166,10 @@ let foo () =
    and the above bar is closing over an nonportable record. Once we allow mutable()
    syntax, we can test this. *)
 [%%expect{|
-val foo : unit -> unit = <fun>
+Line 2, characters 23-61:
+2 |     let r @ portable = {a = best_bytes (); b = best_bytes ()} in
+                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This value is "nonportable" but expected to be "portable".
 |}]
 
 

testsuite/tests/typing-modes/val_modalities.ml

@@ -34,7 +34,7 @@ module M = struct
   let foo = {x = "hello"}
 end
 [%%expect{|
-module M : sig val foo : r @@ global many portable end
+module M : sig val foo : r @@ global many end
 |}]
 
 module type S = sig

testsuite/tests/typing-unique/overwriting.ml

@@ -787,6 +787,17 @@ Error: Overwrite may not change the tag to OptionA.
 Hint: The old tag of this allocation is unknown.
 |}]
 
+(*****************************)
+(* Overwriting with mutation *)
+
+(* Currently all tests in this section fail because mutable record fields
+   are always aliased. But in the future, this will change!
+   When mutable record fields can be unique, we have to ensure that users
+   cannot change the tag using mutation before overwriting a cell with the
+   knowledge of the old tag. We took that into account when designing this
+   feature and all tests here should work correctly in that case.
+   You can find the expected test outputs at PR3157. *)
+
 type 'a mutable_record = { mutable m : 'a }
 
 let mutable_field_aliased r =
@@ -803,8 +814,10 @@ val mutable_field_aliased :
 let mutable_field_aliased r =
   unique_ r.m
 [%%expect{|
-val mutable_field_aliased : 'a mutable_record @ unique -> 'a @@ global many =
-  <fun>
+Line 2, characters 10-13:
+2 |   unique_ r.m
+              ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let tag_of_mutable_field r =
@@ -813,12 +826,10 @@ let tag_of_mutable_field r =
     overwrite_ r.m with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 4, characters 4-33:
+Line 4, characters 15-18:
 4 |     overwrite_ r.m with OptionA s
-        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Alert Translcore: Overwrite not implemented.
-Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
-
+                   ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_seq r =
@@ -828,11 +839,10 @@ let mutating_tag_seq r =
     overwrite_ r.m with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 24-31:
+Line 5, characters 15-18:
 5 |     overwrite_ r.m with OptionA s
-                            ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation was changed through mutation.
+                   ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_seq_same r =
@@ -842,11 +852,10 @@ let mutating_tag_seq_same r =
     overwrite_ r.m with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 24-31:
+Line 5, characters 15-18:
 5 |     overwrite_ r.m with OptionA s
-                            ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation was changed through mutation.
+                   ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_seq_parent r =
@@ -856,11 +865,10 @@ let mutating_tag_seq_parent r =
     overwrite_ r.m.x with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 26-33:
+Line 5, characters 15-20:
 5 |     overwrite_ r.m.x with OptionA s
-                              ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation was changed through mutation.
+                   ^^^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_par r =
@@ -869,11 +877,10 @@ let mutating_tag_par r =
     (r.m <- OptionB s), overwrite_ r.m with OptionA s
   | _ -> (), OptionB ""
 [%%expect{|
-Line 4, characters 44-51:
+Line 4, characters 35-38:
 4 |     (r.m <- OptionB s), overwrite_ r.m with OptionA s
-                                                ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation is being changed through mutation.
+                                       ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_par_parent r =
@@ -882,11 +889,10 @@ let mutating_tag_par_parent r =
     (r.m <- { x = OptionB s }), overwrite_ r.m.x with OptionA s
   | _ -> (), OptionB ""
 [%%expect{|
-Line 4, characters 54-61:
+Line 4, characters 43-48:
 4 |     (r.m <- { x = OptionB s }), overwrite_ r.m.x with OptionA s
-                                                          ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation is being changed through mutation.
+                                               ^^^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_choice r =
@@ -896,12 +902,10 @@ let mutating_tag_choice r =
             else overwrite_ r.m with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 17-46:
+Line 5, characters 28-31:
 5 |             else overwrite_ r.m with OptionA s
-                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Alert Translcore: Overwrite not implemented.
-Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
-
+                                ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_choice_parent r =
@@ -911,12 +915,10 @@ let mutating_tag_choice_parent r =
     else overwrite_ r.m.x with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 9-40:
+Line 5, characters 20-25:
 5 |     else overwrite_ r.m.x with OptionA s
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Alert Translcore: Overwrite not implemented.
-Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
-
+                        ^^^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_choice_seq r =
@@ -926,11 +928,10 @@ let mutating_tag_choice_seq r =
     overwrite_ r.m with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 24-31:
+Line 5, characters 15-18:
 5 |     overwrite_ r.m with OptionA s
-                            ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation was changed through mutation.
+                   ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let mutating_tag_choice_seq_parent r =
@@ -940,11 +941,10 @@ let mutating_tag_choice_seq_parent r =
     overwrite_ r.m.x with OptionA s
   | _ -> OptionB ""
 [%%expect{|
-Line 5, characters 26-33:
+Line 5, characters 15-20:
 5 |     overwrite_ r.m.x with OptionA s
-                              ^^^^^^^
-Error: Overwrite may not change the tag to OptionA.
-Hint: The old tag of this allocation was changed through mutation.
+                   ^^^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 
@@ -959,12 +959,10 @@ let mutating_tag_rematch r =
     end
   | _ -> OptionB ""
 [%%expect{|
-Line 7, characters 6-35:
+Line 7, characters 17-20:
 7 |       overwrite_ r.m with OptionB s
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Alert Translcore: Overwrite not implemented.
-Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
-
+                     ^^^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 (********************************)

testsuite/tests/typing-unique/unique.ml

@@ -597,15 +597,7 @@ let array_pats (arr : int option array) =
   | [| o |] -> let _ = unique_id arr in aliased_id o
   | _ -> None
 [%%expect{|
-Line 3, characters 51-52:
-3 |   | [| o |] -> let _ = unique_id arr in aliased_id o
-                                                       ^
-Error: This value is used here,
-       but it is part of a value that has already been used as unique:
-Line 3, characters 33-36:
-3 |   | [| o |] -> let _ = unique_id arr in aliased_id o
-                                     ^^^
-
+val array_pats : int option array @ unique -> int option = <fun>
 |}]
 
 let array_pats (arr : int option iarray) =

typing/typecore.ml

@@ -971,21 +971,21 @@ let apply_mode_annots ~loc ~env (m : Alloc.Const.Option.t) mode =
   | Error e -> error (Right_le_left, e))
 
 (** Given the parameter [m0] on mutable, return the mode of future writes. *)
-(* CR uniqueness: change back to old implementation *)
-let mutable_mode _m0 rmode =
-  rmode
-    |> Value.meet_with (Comonadic Areality) (Regionality.Const.legacy)
-    |> Value.meet_with (Comonadic Linearity) (Linearity.Const.legacy)
-    |> Value.meet_with (Comonadic Portability) (Portability.Const.legacy)
-    |> Value.join_with (Monadic Contention) (Contention.Const.legacy)
+let mutable_mode m0 =
+  let m0 =
+    Alloc.Const.merge
+      {comonadic = m0;
+       monadic = Alloc.Monadic.Const.min}
+  in
+  m0 |> Const.alloc_as_value |> Value.of_const
 
 (** Takes the mutability on a field, and expected mode of the record (adjusted
     for allocation), check that the construction would be allowed. *)
 let check_construct_mutability ~loc ~env mutability argument_mode =
   match mutability with
   | Immutable -> ()
   | Mutable m0 ->
-      let m0 = mutable_mode m0 (Value.newvar ()) in
+      let m0 = mutable_mode m0 in
       submode ~loc ~env m0 argument_mode
 
 (** The [expected_mode] of the record when projecting a mutable field. *)
@@ -5882,7 +5882,7 @@ and type_expect_
         match label.lbl_mut with
         | Mutable m0 ->
           submode ~loc:record.exp_loc ~env rmode mode_mutate_mutable;
-          let mode = mutable_mode m0 rmode |> mode_default in
+          let mode = mutable_mode m0 |> mode_default in
           let mode = mode_modality label.lbl_modalities mode in
           type_label_exp ~overwrite:No_overwrite_label false env mode loc ty_record
             (lid, label, snewval)

typing/typemode.ml

@@ -191,8 +191,7 @@ let mutable_implied_modalities (mut : Types.mutability) attrs =
       Atom (Comonadic Portability, Meet_with Portability.Const.legacy) ]
   in
   let monadic : Modality.t list =
-    (* CR uniqueness: change back to old implementation *)
-    [ Atom (Monadic Uniqueness, Join_with Uniqueness.Const.Unique);
+    [ Atom (Monadic Uniqueness, Join_with Uniqueness.Const.legacy);
       Atom (Monadic Contention, Join_with Contention.Const.legacy) ]
   in
   match mut with