diff --git a/parsing/builtin_attributes.ml b/parsing/builtin_attributes.ml
index 1c21cd53521..c3d5989f9fd 100644
--- a/parsing/builtin_attributes.ml
+++ b/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
 
diff --git a/parsing/builtin_attributes.mli b/parsing/builtin_attributes.mli
index abe5ba0d1dc..0ee683718fe 100644
--- a/parsing/builtin_attributes.mli
+++ b/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
diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml
index b597aebd6ec..8921a2f20f7 100644
--- a/testsuite/tests/parsetree/source_jane_street.ml
+++ b/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 }
diff --git a/testsuite/tests/typing-jkind-bounds/basics.ml b/testsuite/tests/typing-jkind-bounds/basics.ml
index 09f948d221c..d17789e9bc9 100644
--- a/testsuite/tests/typing-jkind-bounds/basics.ml
+++ b/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
diff --git a/testsuite/tests/typing-layouts/allow_any.ml b/testsuite/tests/typing-layouts/allow_any.ml
index 144f6bc46c2..6866fce712d 100644
--- a/testsuite/tests/typing-layouts/allow_any.ml
+++ b/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
 |}]
 
diff --git a/testsuite/tests/typing-modes/mutable.ml b/testsuite/tests/typing-modes/mutable.ml
index 2424a70ca9e..75d85d99572 100644
--- a/testsuite/tests/typing-modes/mutable.ml
+++ b/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.
diff --git a/testsuite/tests/typing-modes/val_modalities.ml b/testsuite/tests/typing-modes/val_modalities.ml
index 80f199f1f77..2d99fa69c88 100644
--- a/testsuite/tests/typing-modes/val_modalities.ml
+++ b/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 *)
diff --git a/testsuite/tests/warnings/w53.compilers.reference b/testsuite/tests/warnings/w53.compilers.reference
index 18ac9ec83e0..d8dc0e6911d 100644
--- a/testsuite/tests/warnings/w53.compilers.reference
+++ b/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 *)
                      ^^^^^
diff --git a/testsuite/tests/warnings/w53.ml b/testsuite/tests/warnings/w53.ml
index a0b8f043dd6..aba7cc85312 100644
--- a/testsuite/tests/warnings/w53.ml
+++ b/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 *)
diff --git a/typing/jkind.ml b/typing/jkind.ml
index 5d3b5a51d28..9004e567aab 100644
--- a/typing/jkind.ml
+++ b/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;
diff --git a/typing/jkind.mli b/typing/jkind.mli
index c2ffda68b7b..0a7d6a808d4 100644
--- a/typing/jkind.mli
+++ b/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
diff --git a/typing/mode.ml b/typing/mode.ml
index a380b81e4e5..a31c68c736a 100644
--- a/typing/mode.ml
+++ b/typing/mode.ml
@@ -914,12 +914,12 @@ module Lattices_mono = struct
     type ('t, 'r) t =
       | Areality : ('a comonadic_with, 'a) t
       | Linearity : ('areality comonadic_with, Linearity.t) t
+      | Statefulness : ('areality comonadic_with, Statefulness.t) t
       | Portability : ('areality comonadic_with, Portability.t) t
       | Yielding : ('areality comonadic_with, Yielding.t) t
-      | Statefulness : ('areality comonadic_with, Statefulness.t) t
       | Uniqueness : (Monadic_op.t, Uniqueness_op.t) t
-      | Contention : (Monadic_op.t, Contention_op.t) t
       | Visibility : (Monadic_op.t, Visibility_op.t) t
+      | Contention : (Monadic_op.t, Contention_op.t) t
 
     let print : type p r. _ -> (p, r) t -> unit =
      fun ppf -> function
@@ -960,7 +960,7 @@ module Lattices_mono = struct
       | Contention -> t.contention
       | Visibility -> t.visibility
 
-    let update : type p r. (p, r) t -> r -> p -> p =
+    let set : type p r. (p, r) t -> r -> p -> p =
      fun ax r t ->
       match ax with
       | Areality -> { t with areality = r }
@@ -1319,9 +1319,9 @@ module Lattices_mono = struct
     | Visibility.Read -> Statefulness.Observing
     | Visibility.Read_write -> Statefulness.Stateful
 
-  let min_with dst ax a = Axis.update ax a (min dst)
+  let min_with dst ax a = Axis.set ax a (min dst)
 
-  let max_with dst ax a = Axis.update ax a (max dst)
+  let max_with dst ax a = Axis.set ax a (max dst)
 
   let monadic_to_comonadic_min :
       type a. a comonadic_with obj -> Monadic_op.t -> a comonadic_with =
@@ -2078,9 +2078,9 @@ module BiHeyting_Product (L : BiHeyting) = struct
 
   type 'a axis = (t, 'a) Axis.t
 
-  let min_with ax c = Axis.update ax c min
+  let min_with ax c = Axis.set ax c min
 
-  let max_with ax c = Axis.update ax c max
+  let max_with ax c = Axis.set ax c max
 
   let min_axis ax = Axis.proj ax min
 
@@ -2349,10 +2349,11 @@ module Value_with (Areality : Areality) = struct
 
     let all =
       [ P (Comonadic Areality);
-        P (Monadic Uniqueness);
         P (Comonadic Linearity);
-        P (Monadic Contention);
+        P (Monadic Uniqueness);
         P (Comonadic Portability);
+        P (Monadic Contention);
+        P (Comonadic Yielding);
         P (Comonadic Statefulness);
         P (Monadic Visibility) ]
   end
@@ -3023,13 +3024,6 @@ module Modality = struct
             Error
               (Error (ax, { left = Join_with left; right = Join_with right }))
 
-      let compose : type a. a axis -> a raw -> t -> t =
-       fun ax a t ->
-        match a, t with
-        | Join_with c0, Join_const c ->
-          Join_const (Mode.Const.join (Mode.Const.min_with ax c0) c)
-        | Meet_with _, Join_const _ -> assert false
-
       let concat ~then_ t =
         match then_, t with
         | Join_const c0, Join_const c1 -> Join_const (Mode.Const.join c0 c1)
@@ -3037,17 +3031,12 @@ module Modality = struct
       let apply : type l r. t -> (l * r) Mode.t -> (l * r) Mode.t =
        fun t x -> match t with Join_const c -> Mode.join_const c x
 
-      let to_list = function
-        | Join_const c ->
-          [ (let ax : _ Axis.t = Uniqueness in
-             Atom (Monadic ax, Join_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Contention in
-             Atom (Monadic ax, Join_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Visibility in
-             Atom (Monadic ax, Join_with (Axis.proj ax c))) ]
+      let proj ax (Join_const c) = Join_with (Axis.proj ax c)
 
-      let proj ax = function
-        | Join_const c -> Atom (Monadic ax, Join_with (Axis.proj ax c))
+      let set ax a (Join_const c) =
+        match a with
+        | Join_with a -> Join_const (Axis.set ax a c)
+        | Meet_with _ -> assert false
 
       let print ppf = function
         | Join_const c -> Format.fprintf ppf "join_const(%a)" Mode.Const.print c
@@ -3178,13 +3167,6 @@ module Modality = struct
             Error
               (Error (ax, { left = Meet_with left; right = Meet_with right }))
 
-      let compose : type a. a axis -> a raw -> t -> t =
-       fun ax a t ->
-        match a, t with
-        | Meet_with c0, Meet_const c ->
-          Meet_const (Mode.Const.meet (Mode.Const.max_with ax c0) c)
-        | Join_with _, Meet_const _ -> assert false
-
       let concat ~then_ t =
         match then_, t with
         | Meet_const c0, Meet_const c1 -> Meet_const (Mode.Const.meet c0 c1)
@@ -3192,21 +3174,12 @@ module Modality = struct
       let apply : type l r. t -> (l * r) Mode.t -> (l * r) Mode.t =
        fun t x -> match t with Meet_const c -> Mode.meet_const c x
 
-      let to_list = function
-        | Meet_const c ->
-          [ (let ax : _ Axis.t = Areality in
-             Atom (Comonadic ax, Meet_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Linearity in
-             Atom (Comonadic ax, Meet_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Portability in
-             Atom (Comonadic ax, Meet_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Yielding in
-             Atom (Comonadic ax, Meet_with (Axis.proj ax c)));
-            (let ax : _ Axis.t = Statefulness in
-             Atom (Comonadic ax, Meet_with (Axis.proj ax c))) ]
-
-      let proj ax = function
-        | Meet_const c -> Atom (Comonadic ax, Meet_with (Axis.proj ax c))
+      let proj ax (Meet_const c) = Meet_with (Axis.proj ax c)
+
+      let set ax a (Meet_const c) =
+        match a with
+        | Meet_with a -> Meet_const (Axis.set ax a c)
+        | Join_with _ -> assert false
 
       let print ppf = function
         | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Mode.Const.print c
@@ -3342,33 +3315,35 @@ module Modality = struct
         let comonadic = Comonadic.apply t.comonadic comonadic in
         { monadic; comonadic }
 
-      let compose ~then_:(Atom (ax, a)) t =
-        match ax with
-        | Monadic ax ->
-          let monadic = Monadic.compose ax a t.monadic in
-          { t with monadic }
-        | Comonadic ax ->
-          let comonadic = Comonadic.compose ax a t.comonadic in
-          { t with comonadic }
-
       let concat ~then_ t =
         let monadic = Monadic.concat ~then_:then_.monadic t.monadic in
         let comonadic = Comonadic.concat ~then_:then_.comonadic t.comonadic in
         { monadic; comonadic }
 
-      let of_list = List.fold_left (fun m atom -> compose m ~then_:atom) id
-
-      let singleton a = compose ~then_:a id
-
-      let to_list { monadic; comonadic } =
-        Comonadic.to_list comonadic @ Monadic.to_list monadic
-
       let proj (type a d0 d1) (ax : (a, d0, d1) Value.Axis.t)
           { monadic; comonadic } =
         match ax with
         | Monadic ax -> Monadic.proj ax monadic
         | Comonadic ax -> Comonadic.proj ax comonadic
 
+      let set (type a d0 d1) (ax : (a, d0, d1) Value.Axis.t) (a : a raw)
+          { monadic; comonadic } =
+        match ax with
+        | Monadic ax ->
+          let monadic = Monadic.set ax a monadic in
+          { monadic; comonadic }
+        | Comonadic ax ->
+          let comonadic = Comonadic.set ax a comonadic in
+          { monadic; comonadic }
+
+      let diff t0 t1 =
+        List.filter_map
+          (fun (Value.Axis.P ax) ->
+            let a0 = proj ax t0 in
+            let a1 = proj ax t1 in
+            if a0 = a1 then None else Some (Atom (ax, a1)))
+          Value.Axis.all
+
       let print ppf { monadic; comonadic } =
         Format.fprintf ppf "%a;%a" Monadic.print monadic Comonadic.print
           comonadic
@@ -3589,8 +3564,12 @@ module Crossing = struct
       | Modality.Atom (ax, Meet_with c) -> C.print (Value.proj_obj ax) ppf c
     in
     let l =
-      t |> Modality.Value.Const.to_list
-      |> List.filter (fun t -> not @@ Modality.is_id t)
+      List.filter_map
+        (fun (Value.Axis.P ax) ->
+          let a = Modality.Value.Const.proj ax t in
+          let a = Modality.Atom (ax, a) in
+          if Modality.is_id a then None else Some a)
+        Value.Axis.all
     in
     Format.(pp_print_list ~pp_sep:pp_print_space print_atom ppf l)
 end
diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli
index 5913263664f..c3764e5f40b 100644
--- a/typing/mode_intf.mli
+++ b/typing/mode_intf.mli
@@ -373,16 +373,18 @@ module type S = sig
 
   module Axis : sig
     (** ('p, 'r) t represents a projection from a product of type ['p] to an
-    element of type ['r]. *)
+    element of type ['r].
+
+    NB: must listed in the order of axis implication. See [typemode.ml]. *)
     type ('p, 'r) t =
       | Areality : ('a comonadic_with, 'a) t
       | Linearity : ('areality comonadic_with, Linearity.Const.t) t
+      | Statefulness : ('areality comonadic_with, Statefulness.Const.t) t
       | Portability : ('areality comonadic_with, Portability.Const.t) t
       | Yielding : ('areality comonadic_with, Yielding.Const.t) t
-      | Statefulness : ('areality comonadic_with, Statefulness.Const.t) t
       | Uniqueness : (monadic, Uniqueness.Const.t) t
-      | Contention : (monadic, Contention.Const.t) t
       | Visibility : (monadic, Visibility.Const.t) t
+      | Contention : (monadic, Contention.Const.t) t
 
     val print : Format.formatter -> ('p, 'r) t -> unit
 
@@ -640,26 +642,18 @@ module type S = sig
         (** Apply a modality on mode. *)
         val apply : t -> ('l * 'r) Value.t -> ('l * 'r) Value.t
 
-        (** [compose ~then_ t] returns the modality that is [then_] after [t]. *)
-        val compose : then_:atom -> t -> t
-
         (** [concat ~then t] returns the modality that is [then_] after [t]. *)
         val concat : then_:t -> t -> t
 
-        (** [singleton m] returns the modality containing only [m]. *)
-        val singleton : atom -> t
-
-        (** Returns the list of [atom] in the given modality. The list is
-            commutative. Post-condition: each axis is represented in the
-            output list exactly once. *)
-        val to_list : t -> atom list
+        (** [set ax a t] overwrite the [ax] axis of [t] to be [a]. *)
+        val set : ('a, _, _) Value.Axis.t -> 'a raw -> t -> t
 
-        (** Builds up a modality from a list of [atom], by composing each atom with
-            identity. The modalities are applied left to right. *)
-        val of_list : atom list -> t
+        (** Project out the [raw] for the given axis in the given modality. *)
+        val proj : ('a, _, _) Value.Axis.t -> t -> 'a raw
 
-        (** Project out the [atom] for the given axis in the given modality. *)
-        val proj : ('a, _, _) Value.Axis.t -> t -> atom
+        (** [diff t0 t1] returns a list of atoms in [t1] that are different than
+        [t0]. *)
+        val diff : t -> t -> atom list
 
         (** [equate t0 t1] checks that [t0 = t1].
             Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *)
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 8394addb4cb..e64a3154e47 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -1419,14 +1419,14 @@ let tree_of_modality_old (t: Parsetree.modality loc) =
   | Modality "global" -> Some (Ogf_legacy Ogf_global)
   | _ -> None
 
-let tree_of_modalities mut attrs t =
-  let t = Typemode.untransl_modalities mut attrs t in
+let tree_of_modalities mut t =
+  let t = Typemode.untransl_modalities mut t in
   match all_or_none tree_of_modality_old t with
   | Some l -> l
   | None -> List.map tree_of_modality_new t
 
-let tree_of_modalities_new mut attrs t =
-  let l = Typemode.untransl_modalities mut attrs t in
+let tree_of_modalities_new mut t =
+  let l = Typemode.untransl_modalities mut t in
   List.map (fun ({txt = Parsetree.Modality s; _}) -> s) l
 
 (** [tree_of_mode m l] finds the outcome node in [l] that corresponds to [m].
@@ -1643,7 +1643,7 @@ and tree_of_labeled_typlist mode 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_modalities Immutable 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].
@@ -1842,9 +1842,7 @@ let tree_of_label l =
         mut
     | Immutable -> Om_immutable
   in
-  let ld_modalities =
-    tree_of_modalities l.ld_mutable l.ld_attributes l.ld_modalities
-  in
+  let ld_modalities = tree_of_modalities l.ld_mutable 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
@@ -2266,7 +2264,7 @@ let tree_of_value_description id decl =
     { oval_name = id;
       oval_type = Otyp_poly(qtvs, ty);
       oval_modalities =
-        tree_of_modalities_new Immutable decl.val_attributes moda;
+        tree_of_modalities_new Immutable moda;
       oval_prims = [];
       oval_attributes = attrs
     }
diff --git a/typing/typecore.ml b/typing/typecore.ml
index bd421c202bd..567eadc5096 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -2647,7 +2647,7 @@ and type_pat_aux
       solve_Ppat_array ~refine:false loc penv mutability expected_ty
     in
     let modalities =
-      Typemode.transl_modalities ~maturity:Stable mutability [] []
+      Typemode.transl_modalities ~maturity:Stable mutability []
     in
     check_project_mutability ~loc ~env:!!penv mutability alloc_mode.mode;
     let alloc_mode = Modality.Value.Const.apply modalities alloc_mode.mode in
@@ -9515,9 +9515,7 @@ and type_generic_array
     if Types.is_mutable mutability then Predef.type_array
     else Predef.type_iarray
   in
-  let modalities =
-    Typemode.transl_modalities ~maturity:Stable mutability [] []
-  in
+  let modalities = Typemode.transl_modalities ~maturity:Stable mutability [] in
   let argument_mode = mode_modality modalities array_mode in
   let jkind, elt_sort = Jkind.of_new_legacy_sort_var ~why:Array_element in
   let ty = newgenvar jkind in
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 1263bb20e72..c99826ab026 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -490,7 +490,7 @@ let transl_labels (type rep) ~(record_form : rep record_form) ~new_var_jkind
               | Unboxed_product -> raise(Error(loc, Unboxed_mutable_label))
          in
          let modalities =
-          Typemode.transl_modalities ~maturity:Stable mut attrs 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
@@ -531,8 +531,7 @@ let transl_types_gf ~new_var_jkind env loc univars closed cal kloc =
         Mode.Alloc.Const.legacy arg.pca_type
     in
     let gf =
-      Typemode.transl_modalities ~maturity:Stable Immutable []
-        arg.pca_modalities
+      Typemode.transl_modalities ~maturity:Stable Immutable arg.pca_modalities
     in
     {ca_modalities = gf; ca_type = cty; ca_loc = arg.pca_loc}
   in
@@ -3656,8 +3655,7 @@ let transl_value_decl env loc ~sig_modalities valdecl =
   let modalities =
     match valdecl.pval_modalities with
     | [] -> sig_modalities
-    | l -> Typemode.transl_modalities ~maturity:Stable Immutable
-        valdecl.pval_attributes l
+    | l -> Typemode.transl_modalities ~maturity:Stable Immutable l
   in
   let modalities = Mode.Modality.Value.of_const modalities in
   (* CR layouts v5: relax this to check for representability. *)
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 8445017cb72..2bd184a302c 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -1062,7 +1062,7 @@ let apply_pmd_modalities env sig_modalities pmd_modalities mty =
     match pmd_modalities with
     | [] -> sig_modalities
     | _ :: _ ->
-      Typemode.transl_modalities ~maturity:Stable Immutable [] pmd_modalities
+      Typemode.transl_modalities ~maturity:Stable Immutable pmd_modalities
   in
   (*
   Workaround for pmd_modalities
@@ -1268,7 +1268,7 @@ and approx_sig_items env ssg=
                 | [] -> sg
                 | _ ->
                   let modalities =
-                    Typemode.transl_modalities ~maturity:Stable Immutable [] moda
+                    Typemode.transl_modalities ~maturity:Stable Immutable moda
                   in
                   let recursive =
                     not @@ Builtin_attributes.has_attribute "no_recursive_modalities" attrs
@@ -1770,7 +1770,7 @@ and transl_signature env {psg_items; psg_modalities; psg_loc} =
   let names = Signature_names.create () in
 
   let sig_modalities =
-      Typemode.transl_modalities ~maturity:Stable Immutable [] psg_modalities
+      Typemode.transl_modalities ~maturity:Stable Immutable psg_modalities
   in
 
   let transl_include ~loc env sig_acc sincl modalities =
@@ -1796,7 +1796,7 @@ and transl_signature env {psg_items; psg_modalities; psg_loc} =
       match modalities with
       | [] -> sig_modalities
       | _ ->
-        Typemode.transl_modalities ~maturity:Stable Immutable [] modalities
+        Typemode.transl_modalities ~maturity:Stable Immutable modalities
     in
     let sg =
       if not @@ Mode.Modality.Value.Const.is_id modalities then
diff --git a/typing/typemode.ml b/typing/typemode.ml
index 7f77aa58258..3729d4add1d 100644
--- a/typing/typemode.ml
+++ b/typing/typemode.ml
@@ -407,11 +407,10 @@ let untransl_modality (a : Modality.t) : Parsetree.modality loc =
 
 (* For now, mutable implies legacy modalities for both comonadic axes and
    monadic axes. In the future, implications on the comonadic axes will be
-   removed (and can be experimented currently with using
-   @no_mutable_implied_modalities). The implications on the monadic axes will
-   stay. *)
+   removed. The implications on the monadic axes will stay. Implied modalities
+   can be overriden. *)
 (* CR zqian: decouple mutable and comonadic modalities *)
-let mutable_implied_modalities (mut : Types.mutability) attrs =
+let mutable_implied_modalities (mut : Types.mutability) =
   let comonadic : Modality.t list =
     [ Atom (Comonadic Areality, Meet_with Regionality.Const.legacy);
       Atom (Comonadic Linearity, Meet_with Linearity.Const.legacy);
@@ -424,194 +423,73 @@ let mutable_implied_modalities (mut : Types.mutability) attrs =
       Atom (Monadic Contention, Join_with Contention.Const.legacy);
       Atom (Monadic Visibility, Join_with Visibility.Const.legacy) ]
   in
-  match mut with
-  | Immutable -> []
-  | Mutable _ ->
-    if Builtin_attributes.has_no_mutable_implied_modalities attrs
-    then monadic
-    else monadic @ comonadic
+  match mut with Immutable -> [] | Mutable _ -> monadic @ comonadic
+
+let mutable_implied_modalities (mut : Types.mutability) =
+  let l = mutable_implied_modalities mut in
+  List.fold_left
+    (fun t (Modality.Atom (ax, a)) -> Modality.Value.Const.set ax a t)
+    Modality.Value.Const.id l
 
 (* Since [yielding] is the default mode in presence of [local],
    the [global] modality must also apply [unyielding] unless specified.
 
    Similarly for [visibility]/[contention] and [statefulness]/[portability]. *)
-let default_modalities (modalities : Modality.t list) =
-  let areality =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Areality, Meet_with a) ->
-          Some (a : Regionality.Const.t)
-        | _ -> None)
-      modalities
-  in
-  let yielding =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Yielding, Meet_with y) ->
-          Some (y : Yielding.Const.t)
-        | _ -> None)
-      modalities
-  in
-  let visibility =
-    List.find_map
-      (function
-        | Modality.Atom (Monadic Visibility, Join_with a) ->
-          Some (a : Visibility.Const.t)
-        | _ -> None)
-      modalities
-  in
-  let statefulness =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Statefulness, Meet_with s) ->
-          Some (s : Statefulness.Const.t)
-        | _ -> None)
-      modalities
-  in
-  let contention =
-    List.find_map
-      (function
-        | Modality.Atom (Monadic Contention, Join_with c) ->
-          Some (c : Contention.Const.t)
-        | _ -> None)
-      modalities
-  in
-  let portability =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Portability, Meet_with p) ->
-          Some (p : Portability.Const.t)
-        | _ -> None)
-      modalities
-  in
-  (* Build the list of extra modalities *)
-  let extra =
-    (match areality, yielding with
-    | Some Global, None ->
-      [Modality.Atom (Comonadic Yielding, Meet_with Yielding.Const.Unyielding)]
-    | _, _ -> [])
-    @ (match visibility, contention with
-      | Some Visibility.Const.Immutable, None ->
-        [ Modality.Atom
-            (Monadic Contention, Join_with Contention.Const.Contended) ]
-      | Some Visibility.Const.Read, None ->
-        [Modality.Atom (Monadic Contention, Join_with Contention.Const.Shared)]
-      | _, _ -> [])
-    @
-    match statefulness, portability with
-    | Some Statefulness.Const.Stateless, None ->
-      [ Modality.Atom
-          (Comonadic Portability, Meet_with Portability.Const.Portable) ]
-    | _, _ -> []
-  in
-  modalities @ extra
+let implied_modalities (Atom (ax, a) : Modality.t) : Modality.t list =
+  match ax, a with
+  | Comonadic Areality, Meet_with a ->
+    let b : Yielding.Const.t =
+      match a with
+      | Global -> Unyielding
+      | Local -> Yielding
+      | Regional -> assert false
+    in
+    [Atom (Comonadic Yielding, Meet_with b)]
+  | Monadic Visibility, Join_with a ->
+    let b : Contention.Const.t =
+      match a with
+      | Immutable -> Contended
+      | Read -> Shared
+      | Read_write -> Uncontended
+    in
+    [Atom (Monadic Contention, Join_with b)]
+  | Comonadic Statefulness, Meet_with a ->
+    let b : Portability.Const.t =
+      match a with Stateless -> Portable | Stateful | Observing -> Nonportable
+    in
+    [Atom (Comonadic Portability, Meet_with b)]
+  | _ -> []
 
-let transl_modalities ~maturity mut attrs modalities =
-  let mut_modalities = mutable_implied_modalities mut attrs in
+let transl_modalities ~maturity mut modalities =
+  let mut_modalities = mutable_implied_modalities mut in
   let modalities = List.map (transl_modality ~maturity) modalities in
-  let modalities = default_modalities modalities in
-  (* mut_modalities is applied before explicit modalities *)
-  Modality.Value.Const.id
-  |> List.fold_right
-       (fun atom m -> Modality.Value.Const.compose ~then_:atom m)
-       mut_modalities
-  (* For explicit modalities:
-     type r = { x : string @@ foo bar hello }
-     is interpreted as
-     x = foo (bar (hello (r))) *)
-  |> List.fold_right
-       (fun atom m -> Modality.Value.Const.compose ~then_:atom m)
-       modalities
-
-let untransl_yielding l =
-  let areality =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Areality, Meet_with a) ->
-          Some (a : Regionality.Const.t)
-        | _ -> None)
-      l
-  in
-  let yielding =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Yielding, Meet_with y) ->
-          Some (y : Yielding.Const.t)
-        | _ -> None)
-      l
-  in
-  match areality, yielding with
-  | Some Global, Some Unyielding | Some Local, Some Yielding -> None
-  | _, Some yld -> Some (Modality.Atom (Comonadic Yielding, Meet_with yld))
-  | _, None -> None
-
-let untransl_contention l =
-  let visibility =
-    List.find_map
-      (function
-        | Modality.Atom (Monadic Visibility, Join_with a) ->
-          Some (a : Visibility.Const.t)
-        | _ -> None)
-      l
-  in
-  let contention =
-    List.find_map
-      (function
-        | Modality.Atom (Monadic Contention, Join_with c) ->
-          Some (c : Contention.Const.t)
-        | _ -> None)
-      l
-  in
-  match visibility, contention with
-  | Some Visibility.Const.Immutable, Some Contention.Const.Contended
-  | Some Visibility.Const.Read, Some Contention.Const.Shared
-  | Some Visibility.Const.Read_write, Some Contention.Const.Uncontended ->
-    None
-  | _, Some cnt -> Some (Modality.Atom (Monadic Contention, Join_with cnt))
-  | _, None -> None
-
-let untransl_portability l =
-  let statefulness =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Statefulness, Meet_with s) ->
-          Some (s : Statefulness.Const.t)
-        | _ -> None)
-      l
-  in
-  let portability =
-    List.find_map
-      (function
-        | Modality.Atom (Comonadic Portability, Meet_with p) ->
-          Some (p : Portability.Const.t)
-        | _ -> None)
-      l
-  in
-  match statefulness, portability with
-  | Some Statefulness.Const.Stateless, Some Portability.Const.Portable
-  | ( Some Statefulness.Const.(Observing | Stateful),
-      Some Portability.Const.Nonportable ) ->
-    None
-  | _, Some port -> Some (Modality.Atom (Comonadic Portability, Meet_with port))
-  | _, None -> None
-
-let untransl_modalities mut attrs t =
-  let l = Modality.Value.Const.to_list t in
-  let l =
-    (* [filter_map] instead of [filter] + [append] to preserve order. *)
-    List.filter_map
-      (function
-        | Modality.Atom (Comonadic Yielding, _) -> untransl_yielding l
-        | Modality.Atom (Monadic Contention, _) -> untransl_contention l
-        | Modality.Atom (Comonadic Portability, _) -> untransl_portability l
-        | a when Modality.is_id a -> None
-        | a -> Some a)
-      l
+  (* axes listed in the order of implication. *)
+  let modalities =
+    List.stable_sort
+      (fun (Modality.Atom (ax0, _)) (Modality.Atom (ax1, _)) ->
+        Stdlib.compare (Value.Axis.P ax0) (Value.Axis.P ax1))
+      modalities
   in
-  let mut_modalities = mutable_implied_modalities mut attrs in
-  (* polymorphic equality suffices for now. *)
-  let l = List.filter (fun x -> not @@ List.mem x mut_modalities) l in
-  List.map untransl_modality l
+  let open Modality in
+  (* - mut_modalities is applied before explicit modalities.
+     - explicit modalities can override mut_modalities.
+     - For the same axis, later modalities overrides earlier modalities. *)
+  (* CR zqian: warn if an axis is specified multiple times in a modality expr. *)
+  List.fold_left
+    (fun m (Atom (ax, a) as t) ->
+      let m = Value.Const.set ax a m in
+      List.fold_left
+        (fun m (Atom (ax, a)) -> Value.Const.set ax a m)
+        m (implied_modalities t))
+    mut_modalities modalities
+
+let untransl_modalities mut t =
+  let mut_modalities = mutable_implied_modalities mut in
+  let l = Modality.Value.Const.diff mut_modalities t in
+  let implied = List.concat_map implied_modalities l in
+  l
+  |> List.filter (fun x -> not @@ List.mem x implied)
+  |> List.map untransl_modality
 
 let transl_alloc_mode modes =
   let opt = transl_mode_annots modes in
diff --git a/typing/typemode.mli b/typing/typemode.mli
index a39eb490192..9a3a5753bc4 100644
--- a/typing/typemode.mli
+++ b/typing/typemode.mli
@@ -14,7 +14,6 @@ val transl_alloc_mode : Parsetree.modes -> Mode.Alloc.Const.t
 val transl_modalities :
   maturity:Language_extension.maturity ->
   Types.mutability ->
-  Parsetree.attributes ->
   Parsetree.modalities ->
   Mode.Modality.Value.Const.t
 
@@ -24,10 +23,7 @@ val untransl_modality : Mode.Modality.t -> Parsetree.modality Location.loc
     attributes on the field and remove mutable-implied modalities accordingly.
     *)
 val untransl_modalities :
-  Types.mutability ->
-  Parsetree.attributes ->
-  Mode.Modality.Value.Const.t ->
-  Parsetree.modalities
+  Types.mutability -> Mode.Modality.Value.Const.t -> Parsetree.modalities
 
 module Transled_modifiers : sig
   type t =
diff --git a/typing/uniqueness_analysis.ml b/typing/uniqueness_analysis.ml
index cfa37cce07c..e6aaf2b9907 100644
--- a/typing/uniqueness_analysis.ml
+++ b/typing/uniqueness_analysis.ml
@@ -1532,20 +1532,14 @@ end = struct
 
   let child proj t = List.map (UF.Path.child proj) t
 
-  let modal_child gf proj t =
+  let modal_child modalities proj t =
     (* CR zqian: Instead of just ignoring such children, we should add modality
        to [Projection.t] and add corresponding logic in [UsageTree]. *)
-    let gf = Modality.Value.Const.to_list gf in
-    let l =
-      List.filter
-        (function
-         | Atom (Monadic Uniqueness, Join_with Aliased) -> true
-         | Atom (Comonadic Linearity, Meet_with Many) -> true
-         | _ -> false
-          : Modality.t -> _)
-        gf
-    in
-    if List.length l = 2 then untracked else child proj t
+    let uni = Modality.Value.Const.proj (Monadic Uniqueness) modalities in
+    let lin = Modality.Value.Const.proj (Comonadic Linearity) modalities in
+    match uni, lin with
+    | Join_with Aliased, Meet_with Many -> untracked
+    | _ -> child proj t
 
   let tuple_field i t = child (Projection.Tuple_field i) t
 
@@ -1560,7 +1554,7 @@ end = struct
   let variant_field s t = child (Projection.Variant_field s) t
 
   let array_index mut i t =
-    let modality = Typemode.transl_modalities ~maturity:Stable mut [] [] in
+    let modality = Typemode.transl_modalities ~maturity:Stable mut [] in
     modal_child modality (Projection.Array_index i) t
 
   let memory_address t = child Projection.Memory_address t
diff --git a/typing/untypeast.ml b/typing/untypeast.ml
index b5ccf59f5a5..f9adfded7ce 100644
--- a/typing/untypeast.ml
+++ b/typing/untypeast.ml
@@ -253,7 +253,7 @@ let type_kind sub tk = match tk with
 
 let constructor_argument sub {ca_loc; ca_type; ca_modalities} =
   let loc = sub.location sub ca_loc in
-  let pca_modalities = Typemode.untransl_modalities Immutable [] ca_modalities in
+  let pca_modalities = Typemode.untransl_modalities Immutable ca_modalities in
   { pca_loc = loc; pca_type = sub.typ sub ca_type; pca_modalities }
 
 let constructor_arguments sub = function
@@ -285,8 +285,7 @@ let label_declaration sub ld =
   let attrs = sub.attributes sub ld.ld_attributes in
   let mut = mutable_ ld.ld_mutable in
   let modalities =
-    Typemode.untransl_modalities ld.ld_mutable ld.ld_attributes
-      ld.ld_modalities
+    Typemode.untransl_modalities ld.ld_mutable ld.ld_modalities
   in
   Type.field ~loc ~attrs ~mut ~modalities
     (map_loc sub ld.ld_name)
@@ -743,7 +742,7 @@ let module_type_declaration sub mtd =
 
 let signature sub {sig_items; sig_modalities; sig_sloc} =
   let psg_items = List.map (sub.signature_item sub) sig_items in
-  let psg_modalities = Typemode.untransl_modalities Immutable [] sig_modalities in
+  let psg_modalities = Typemode.untransl_modalities Immutable sig_modalities in
   let psg_loc = sub.location sub sig_sloc in
   {psg_items; psg_modalities; psg_loc}
 
@@ -774,7 +773,7 @@ let signature_item sub item =
     | Tsig_open od ->
         Psig_open (sub.open_description sub od)
     | Tsig_include (incl, moda) ->
-        let pmoda = Typemode.untransl_modalities Immutable [] moda in
+        let pmoda = Typemode.untransl_modalities Immutable moda in
         Psig_include (sub.include_description sub incl, pmoda)
     | Tsig_class list ->
         Psig_class (List.map (sub.class_description sub) list)