diff --git a/native_toplevel/opttoploop.ml b/native_toplevel/opttoploop.ml
index cb38e020220..a7138a460f5 100644
--- a/native_toplevel/opttoploop.ml
+++ b/native_toplevel/opttoploop.ml
@@ -345,7 +345,7 @@ let name_expression ~loc ~attrs sort exp =
       val_loc = loc;
       val_attributes = attrs;
       val_zero_alloc = Default_zero_alloc;
-      val_modalities = Mode.Modality.Value.id |> Mode.Modality.Value.internalize;
+      val_modalities = Mode.Modality.Value.id;
       val_uid = Uid.internal_not_actually_unique; }
   in
   let sg = [Sig_value(id, vd, Exported)] in
diff --git a/ocaml/lambda/lambda.ml b/ocaml/lambda/lambda.ml
index 0e7898834b8..f6407cd24fe 100644
--- a/ocaml/lambda/lambda.ml
+++ b/ocaml/lambda/lambda.ml
@@ -1402,7 +1402,7 @@ let build_substs update_env ?(freshen_bound_variables = false) s =
         let env_updates =
           let find_in_old id =
             let vd = Env.find_value (Path.Pident id) old_env in
-            let vd = {vd with val_modalities = Mode.Modality.Value.id'} in
+            let vd = {vd with val_modalities = Mode.Modality.Value.id} in
             let mode = Mode.Value.max |> Mode.Value.disallow_right in
             (vd, mode)
           in
diff --git a/ocaml/ocamldoc/odoc_sig.ml b/ocaml/ocamldoc/odoc_sig.ml
index 856feaf3d2c..8ca23cc6089 100644
--- a/ocaml/ocamldoc/odoc_sig.ml
+++ b/ocaml/ocamldoc/odoc_sig.ml
@@ -492,7 +492,7 @@ module Analyser =
       let record comments
           { Typedtree.ld_id; ld_mutable; ld_type; ld_loc; ld_attributes } =
         get_field env comments @@
-        {Types.ld_id; ld_mutable; ld_modalities = Mode.Modality.Value.id;
+        {Types.ld_id; ld_mutable; ld_modalities = Mode.Modality.Value.Const.id;
          ld_jkind=Jkind.any ~why:Dummy_jkind (* ignored *);
          ld_type=ld_type.Typedtree.ctyp_type;
          ld_loc; ld_attributes; ld_uid=Types.Uid.internal_not_actually_unique} in
diff --git a/ocaml/typing/datarepr.ml b/ocaml/typing/datarepr.ml
index df486cb212b..52082d467e0 100644
--- a/ocaml/typing/datarepr.ml
+++ b/ocaml/typing/datarepr.ml
@@ -97,7 +97,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep =
       [
         {
           ca_type = newgenconstr path type_params;
-          ca_modalities = Mode.Modality.Value.id;
+          ca_modalities = Mode.Modality.Value.Const.id;
           ca_loc = Location.none
         }
       ],
@@ -206,7 +206,7 @@ let none =
 
 let dummy_label =
   { lbl_name = ""; lbl_res = none; lbl_arg = none;
-    lbl_mut = Immutable; lbl_modalities = Mode.Modality.Value.id;
+    lbl_mut = Immutable; lbl_modalities = Mode.Modality.Value.Const.id;
     lbl_jkind = Jkind.any ~why:Dummy_jkind;
     lbl_num = -1; lbl_pos = -1; lbl_all = [||];
     lbl_repres = Record_unboxed;
diff --git a/ocaml/typing/env.ml b/ocaml/typing/env.ml
index a4cbe881914..efb18bc23a6 100644
--- a/ocaml/typing/env.ml
+++ b/ocaml/typing/env.ml
@@ -906,9 +906,9 @@ let normalize_vda_mode vda =
   let vda_description = vda.vda_description in
   let modalities = vda_description.val_modalities in
   let vda_description =
-    {vda_description with val_modalities = Mode.Modality.Value.id'}
+    {vda_description with val_modalities = Mode.Modality.Value.id}
   in
-  let vda_mode = Mode.Modality.Value.apply_left modalities vda.vda_mode in
+  let vda_mode = Mode.Modality.Value.apply modalities vda.vda_mode in
   {vda with vda_description; vda_mode}
 
 (* Print addresses *)
@@ -2040,7 +2040,6 @@ and store_value ?check ~mode id addr decl shape env =
   Option.iter
     (fun f -> check_usage decl.val_loc id decl.val_uid f !value_declarations)
     check;
-  let _ = Mode.Modality.Value.apply_left decl.val_modalities mode in
   let vda =
     { vda_description = decl;
       vda_address = addr;
diff --git a/ocaml/typing/includecore.ml b/ocaml/typing/includecore.ml
index c2dc47d5bf2..c38c31387ee 100644
--- a/ocaml/typing/includecore.ml
+++ b/ocaml/typing/includecore.ml
@@ -653,7 +653,9 @@ module Record_diffing = struct
         begin match mut with
         | Some mut -> Some (Mutability mut)
         | None ->
-          match Modality.Value.equate ld1.ld_modalities ld2.ld_modalities with
+          match
+            Modality.Value.Const.equate ld1.ld_modalities ld2.ld_modalities
+          with
           | Ok () ->
             let tl1 = params1 @ [ld1.ld_type] in
             let tl2 = params2 @ [ld2.ld_type] in
@@ -826,7 +828,7 @@ module Variant_diffing = struct
           | exception Ctype.Equality err -> Some (Type err)
           | () -> List.combine arg1_gfs arg2_gfs
                   |> find_map_idx
-                    (fun (x,y) -> get_error @@ Modality.Value.equate x y)
+                    (fun (x,y) -> get_error @@ Modality.Value.Const.equate x y)
                   |> Option.map (fun (i, err) -> Modality (i, err))
         end
     | Types.Cstr_record l1, Types.Cstr_record l2 ->
diff --git a/ocaml/typing/mode.ml b/ocaml/typing/mode.ml
index 10a105156f4..43d713257f0 100644
--- a/ocaml/typing/mode.ml
+++ b/ocaml/typing/mode.ml
@@ -1258,6 +1258,15 @@ let equate_from_submode submode_log m0 m1 ~log =
     | Ok () -> Ok ())
   [@@inline]
 
+let equate_from_submode' submode m0 m1 =
+  match submode m0 m1 with
+  | Error e -> Error (Left_le_right, e)
+  | Ok () -> (
+    match submode m1 m0 with
+    | Error e -> Error (Right_le_left, e)
+    | Ok () -> Ok ())
+  [@@inline]
+
 module Common (Obj : Obj) = struct
   open Obj
 
@@ -2148,10 +2157,6 @@ let value_to_alloc_r2l m =
   { comonadic; monadic }
 
 module Modality = struct
-  type _internal = private Internal
-
-  type _user = private User
-
   type ('m, 'a) raw =
     | Meet_with : 'a -> (('a, 'l * 'r) mode_comonadic, 'a) raw
     | Join_with : 'a -> (('a, 'l * 'r) mode_monadic, 'a) raw
@@ -2171,45 +2176,62 @@ module Modality = struct
 
   module Monadic = struct
     module Mode = Value.Monadic
-    module Const = Mode.Const
-
-    type 'd t =
-      | Join_const : Const.t -> 'd t
-      | Diff : Mode.lr * Mode.l -> _internal t
-      | Undefined : _internal t
 
-    type user = _user t
+    type 'a axis = (Mode.Const.t, 'a) Axis.t
 
-    type internal = _internal t
-
-    let user_or_internal : type d. d t -> (user, internal) Either.t = function
-      | Join_const _ as m -> Left m
-      | Diff _ as m -> Right m
-      | Undefined as m -> Right m
+    type error =
+      | Error : 'a axis * (('a, _) mode_monadic, 'a) raw Solver.error -> error
 
-    let internalize : type d. d t -> internal = function
-      | Join_const _ as t -> t
-      | Diff _ as t -> t
-      | Undefined as t -> t
+    module Const = struct
+      type t = Join_const of Mode.Const.t
+
+      let id = Join_const Mode.Const.min
+
+      let max = Join_const Mode.Const.max
+
+      let sub left right : (_, error) Result.t =
+        match left, right with
+        | Join_const c0, Join_const c1 ->
+          if Mode.Const.le c0 c1
+          then Ok ()
+          else
+            let (Error (ax, { left; right })) =
+              Mode.axis_of_error { left = c0; right = c1 }
+            in
+            Error
+              (Error (ax, { left = Join_with left; right = Join_with right }))
+
+      let compose :
+          type a l r. a axis -> ((a, l * r) mode_monadic, 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 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))) ]
 
-    type 'a axis = (Const.t, 'a) Axis.t
+      let print ppf = function
+        | Join_const c -> Format.fprintf ppf "join_const(%a)" Mode.Const.print c
+    end
 
-    type error =
-      | Error : 'a axis * (('a, _) mode_monadic, 'a) raw Solver.error -> error
+    type t =
+      | Const of Const.t
+      | Diff of Mode.lr * Mode.l
+      | Undefined
 
-    let sub_any_user_log :
-        type d d'. d t -> d' t -> log:_ -> (unit, error) Result.t =
-     fun left right ~log ->
+    let sub_log left right ~log : (unit, error) Result.t =
       match left, right with
-      | Join_const c0, Join_const c1 ->
-        if Const.le c0 c1
-        then Ok ()
-        else
-          let (Error (ax, { left; right })) =
-            Mode.axis_of_error { left = c0; right = c1 }
-          in
-          Error (Error (ax, { left = Join_with left; right = Join_with right }))
-      | Diff (mm, m), Join_const c -> (
+      | Const c0, Const c1 -> Const.sub c0 c1
+      | Diff (mm, m), Const (Join_const c) -> (
         (* Check that for any x >= mm, join(x, m) <= join(x, c).
            By definition of join, equivalent to check m <= join(x, c)
            Since x >= mm, equivalent to check m <= join(mm, c). *)
@@ -2227,42 +2249,21 @@ module Modality = struct
            in which case LHS and RHS should be physically equal. *)
         assert (left == right);
         Ok ()
-      | Join_const _, Diff _ -> assert false
+      | Const _, Diff _ -> assert false
       | Undefined, _ | _, Undefined ->
         Misc.fatal_error "undefined modality should not be inspected."
 
-    let sub_log = sub_any_user_log
-
-    let id = Join_const Const.min
+    let id = Const Const.id
 
-    let cons :
-        type a l r. a axis -> ((a, l * r) mode_monadic, a) raw -> user -> user =
-     fun ax a t ->
-      match a, t with
-      | Join_with c0, Join_const c ->
-        Join_const (Const.join (Const.min_with ax c0) c)
-      | Meet_with _, Join_const _ -> assert false
-
-    let apply_user : type l r. user -> (l * r) Mode.t -> (l * r) Mode.t =
-     fun t x -> match t with Join_const c -> Mode.join_const c x
-
-    let apply_left : type d r. d t -> (allowed * r) Mode.t -> Mode.l =
+    let apply : type r. t -> (allowed * r) Mode.t -> Mode.l =
      fun t x ->
       match t with
-      | Join_const c -> Mode.join_const c x |> Mode.disallow_right
+      | Const c -> Const.apply c x |> Mode.disallow_right
       | Undefined -> assert false
       | Diff (_, m) -> Mode.join [m; Mode.disallow_right x]
 
-    let to_list : user -> _ = 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 print : type d. _ -> d t -> unit =
-     fun ppf -> function
-      | Join_const c -> Format.fprintf ppf "join_const(%a)" Const.print c
+    let print ppf = function
+      | Const c -> Const.print ppf c
       | Undefined -> Format.fprintf ppf "undefined"
       | Diff _ -> Format.fprintf ppf "diff"
 
@@ -2270,68 +2271,92 @@ module Modality = struct
       (* We will be producing [join x m] for any [x >= mm].
          We want to find the minimal [m'] such that [join x m <= join x m'] for any [x >= mm].
          Or equivalently [m <= join x m'] for any [x >= mm].
-         Suffices if [m <= join mm m'].
-         Suffices if [m <= join mm.lower m'].
+         Equivalently [m <= join mm m'].
+         Equivalently [m <= join mm.lower m'].
          or [subtract mm.lower m <= m'].
       *)
       let mc = Mode.Guts.get_floor mm in
       Mode.subtract mc m
 
-    let zap_to_id : type d. d t -> user = function
-      | Join_const _ as t -> t
+    let zap_to_id = function
+      | Const c -> c
       | Undefined -> assert false
       | Diff (mm, m) ->
         let m' = cross mm m in
         let c = Mode.zap_to_floor m' in
-        Join_const c
+        Const.Join_const c
+
+    let to_const_exn = function
+      | Const c -> c
+      | Undefined | Diff _ -> assert false
 
-    let zap_assert : type d. d t -> user =
-     fun m ->
-      match user_or_internal m with
-      | Left user -> user
-      | Right _ -> assert false
+    let of_const c = Const c
 
     let infer ~md_mode ~mode = Diff (md_mode, mode)
 
-    let max = Join_const Const.max
+    let max = Const Const.max
   end
 
   module Comonadic = struct
     module Mode = Value.Comonadic
-    module Const = Mode.Const
 
-    type 'd t =
-      | Meet_const : Const.t -> 'd t
-      | Undefined : _internal t
-      | Exactly : Mode.lr * Mode.l -> _internal t
+    type 'a axis = (Mode.Const.t, 'a) Axis.t
 
-    type user = _user t
-
-    type internal = _internal t
+    type error =
+      | Error : 'a axis * (('a, _) mode_comonadic, 'a) raw Solver.error -> error
 
-    let user_or_internal : type d. d t -> (user, internal) Either.t = function
-      | Meet_const _ as m -> Left m
-      | Exactly _ as m -> Right m
-      | Undefined as m -> Right m
+    module Const = struct
+      type t = Meet_const of Mode.Const.t
+
+      let id = Meet_const Mode.Const.max
+
+      let max = Meet_const Mode.Const.max
+
+      let sub left right : (_, error) Result.t =
+        match left, right with
+        | Meet_const c0, Meet_const c1 ->
+          if Mode.Const.le c0 c1
+          then Ok ()
+          else
+            let (Error (ax, { left; right })) =
+              Mode.axis_of_error { left = c0; right = c1 }
+            in
+            Error
+              (Error (ax, { left = Meet_with left; right = Meet_with right }))
+
+      let compose :
+          type a l r. a axis -> ((a, l * r) mode_comonadic, 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 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))) ]
 
-    type 'a axis = (Const.t, 'a) Axis.t
+      let print ppf = function
+        | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Mode.Const.print c
+    end
 
-    type error =
-      | Error : 'a axis * (('a, _) mode_comonadic, 'a) raw Solver.error -> error
+    type t =
+      | Const of Const.t
+      | Undefined
+      | Exactly of Mode.lr * Mode.l
 
-    let sub_any_user_log :
-        type d d'. d t -> d' t -> log:_ -> (unit, error) Result.t =
-     fun left right ~log ->
+    let sub_log left right ~log : (unit, error) Result.t =
       match left, right with
-      | Meet_const c0, Meet_const c1 ->
-        if Const.le c0 c1
-        then Ok ()
-        else
-          let (Error (ax, { left; right })) =
-            Mode.axis_of_error { left = c0; right = c1 }
-          in
-          Error (Error (ax, { left = Meet_with left; right = Meet_with right }))
-      | Exactly (_mm, m), Meet_const c -> (
+      | Const c0, Const c1 -> Const.sub c0 c1
+      | Exactly (_mm, m), Const (Meet_const c) -> (
         (* check for any x >= mm, meet(m, x) <= meet(c, x).
            Equivalent to check meet(m, x) <= c.
            Equivalent to check m <= c. *)
@@ -2349,151 +2374,131 @@ module Modality = struct
            in which case LHS and RHS should be physically equal. *)
         assert (left == right);
         Ok ()
-      | Meet_const _, Exactly _ -> assert false
+      | Const _, Exactly _ -> assert false
       | Undefined, _ | _, Undefined -> assert false
 
-    let sub_log left right ~log = sub_any_user_log left right ~log
-
-    let id = Meet_const Const.max
-
-    let cons :
-        type a l r. a axis -> ((a, l * r) mode_comonadic, a) raw -> user -> user
-        =
-     fun ax a t ->
-      match a, t with
-      | Meet_with c0, Meet_const c ->
-        Meet_const (Const.meet (Const.max_with ax c0) c)
-      | Join_with _, Meet_const _ -> assert false
-
-    let internalize : type d. d t -> internal = function
-      | Meet_const _ as t -> t
-      | Exactly _ as t -> t
-      | Undefined as t -> t
-
-    let apply_user : type l r. user -> (l * r) Mode.t -> (l * r) Mode.t =
-     fun t x -> match t with Meet_const c -> Mode.meet_const c x
+    let id = Const Const.id
 
-    let apply_left : type d r. d t -> (allowed * r) Mode.t -> Mode.l =
+    let apply : type r. t -> (allowed * r) Mode.t -> Mode.l =
      fun t x ->
       match t with
-      | Meet_const c -> Mode.meet_const c x |> Mode.disallow_right
+      | Const c -> Const.apply c x |> Mode.disallow_right
       | Undefined -> assert false
       | Exactly (_mm, m) -> m
 
-    let to_list : user -> _ = 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 print : type d. _ -> d t -> unit =
-     fun ppf -> function
-      | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Const.print c
+    let print ppf = function
+      | Const c -> Const.print ppf c
       | Undefined -> Format.fprintf ppf "undefined"
       | Exactly _ -> Format.fprintf ppf "exactly"
 
     let infer ~md_mode ~mode = Exactly (md_mode, mode)
 
-    let max = Meet_const Const.max
+    let max = Const Const.max
 
-    let zap_to_id : type d. d t -> user = function
-      | Meet_const _ as t -> t
+    let zap_to_id = function
+      | Const c -> c
       | Undefined -> assert false
-      | Exactly _ -> id
+      | Exactly _ -> Const.id
+
+    let to_const_exn = function
+      | Const c -> c
+      | Undefined | Exactly _ -> assert false
 
-    let zap_assert m =
-      match user_or_internal m with
-      | Left user -> user
-      | Right _ -> assert false
+    let of_const c = Const c
   end
 
   module Value = struct
-    type 'd t = ('d Monadic.t, 'd Comonadic.t) monadic_comonadic
+    type error =
+      | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error
 
-    type user = _user t
+    type equate_error = equate_step * error
 
-    type internal = _internal t
+    module Const = struct
+      module Monadic = Monadic.Const
+      module Comonadic = Comonadic.Const
 
-    let apply_user t { monadic; comonadic } =
-      let monadic = Monadic.apply_user t.monadic monadic in
-      let comonadic = Comonadic.apply_user t.comonadic comonadic in
-      { monadic; comonadic }
+      type t = (Monadic.t, Comonadic.t) monadic_comonadic
 
-    let apply_left t { monadic; comonadic } =
-      let monadic = Monadic.apply_left t.monadic monadic in
-      let comonadic = Comonadic.apply_left t.comonadic comonadic in
-      { monadic; comonadic }
+      let id = { monadic = Monadic.id; comonadic = Comonadic.id }
 
-    type error =
-      | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error
+      let sub t0 t1 : (unit, error) Result.t =
+        match Monadic.sub t0.monadic t1.monadic with
+        | Error (Error (ax, e)) -> Error (Error (Monadic ax, e))
+        | Ok () -> (
+          match Comonadic.sub t0.comonadic t1.comonadic with
+          | Ok () -> Ok ()
+          | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)))
 
-    let sub_log : type d d'. d t -> d' t -> log:_ -> (unit, error) Result.t =
-     fun t0 t1 ~log ->
-      match Monadic.sub_log t0.monadic t1.monadic ~log with
-      | Error (Error (ax, e)) -> Error (Error (Monadic ax, e))
-      | Ok () -> (
-        match Comonadic.sub_log t0.comonadic t1.comonadic ~log with
-        | Ok () -> Ok ()
-        | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)))
+      let equate = equate_from_submode' sub
 
-    let sub l r = try_with_log (sub_log l r)
+      let apply t { monadic; comonadic } =
+        let monadic = Monadic.apply t.monadic monadic in
+        let comonadic = Comonadic.apply t.comonadic comonadic in
+        { monadic; comonadic }
 
-    type equate_error = equate_step * error
+      let compose (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 equate m0 m1 = try_with_log (equate_from_submode sub_log m0 m1)
+      let singleton a = compose a id
 
-    let id : user = { monadic = Monadic.id; comonadic = Comonadic.id }
+      let to_list { monadic; comonadic } =
+        Comonadic.to_list comonadic @ Monadic.to_list monadic
+    end
 
-    let undefined : internal =
-      { monadic = Undefined; comonadic = Comonadic.Undefined }
+    type t = (Monadic.t, Comonadic.t) monadic_comonadic
 
-    let cons (Atom (ax, a)) t =
-      match ax with
-      | Monadic ax ->
-        let monadic = Monadic.cons ax a t.monadic in
-        { t with monadic }
-      | Comonadic ax ->
-        let comonadic = Comonadic.cons ax a t.comonadic in
-        { t with comonadic }
-
-    let internalize : type d. d t -> internal =
-     fun { monadic; comonadic } ->
-      let monadic = Monadic.internalize monadic in
-      let comonadic = Comonadic.internalize comonadic in
+    let id : t = { monadic = Monadic.id; comonadic = Comonadic.id }
+
+    let undefined : t = { monadic = Undefined; comonadic = Comonadic.Undefined }
+
+    let apply t { monadic; comonadic } =
+      let monadic = Monadic.apply t.monadic monadic in
+      let comonadic = Comonadic.apply t.comonadic comonadic in
       { monadic; comonadic }
 
-    let id' = internalize id
+    let sub_log t0 t1 ~log : (unit, error) Result.t =
+      match Monadic.sub_log t0.monadic t1.monadic ~log with
+      | Error (Error (ax, e)) -> Error (Error (Monadic ax, e))
+      | Ok () -> (
+        match Comonadic.sub_log t0.comonadic t1.comonadic ~log with
+        | Ok () -> Ok ()
+        | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)))
 
-    let singleton a = cons a id
+    let sub l r = try_with_log (sub_log l r)
 
-    let to_list { monadic; comonadic } =
-      Comonadic.to_list comonadic @ Monadic.to_list monadic
+    let equate m0 m1 = try_with_log (equate_from_submode sub_log m0 m1)
 
-    let print ppf ({ monadic; comonadic } : 'd t) =
+    let print ppf ({ monadic; comonadic } : t) =
       Format.fprintf ppf "%a,%a" Monadic.print monadic Comonadic.print comonadic
 
-    let infer : md_mode:Value.lr -> mode:Value.l -> internal =
-     fun ~md_mode ~mode ->
+    let infer ~md_mode ~mode : t =
       let comonadic =
         Comonadic.infer ~md_mode:md_mode.comonadic ~mode:mode.comonadic
       in
       let monadic = Monadic.infer ~md_mode:md_mode.monadic ~mode:mode.monadic in
       { monadic; comonadic }
 
-    let zap_to_id : type d. d t -> user =
-     fun t ->
+    let zap_to_id t =
       let { monadic; comonadic } = t in
       let comonadic = Comonadic.zap_to_id comonadic in
       let monadic = Monadic.zap_to_id monadic in
       { monadic; comonadic }
 
-    let zap_assert : type d. d t -> user =
-     fun { monadic; comonadic } ->
-      let comonadic = Comonadic.zap_assert comonadic in
-      let monadic = Monadic.zap_assert monadic in
+    let to_const_exn t =
+      let { monadic; comonadic } = t in
+      let comonadic = Comonadic.to_const_exn comonadic in
+      let monadic = Monadic.to_const_exn monadic in
+      { monadic; comonadic }
+
+    let of_const { monadic; comonadic } =
+      let comonadic = Comonadic.of_const comonadic in
+      let monadic = Monadic.of_const monadic in
       { monadic; comonadic }
 
     let max =
diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli
index 2e7cc939358..fe39d2dc422 100644
--- a/ocaml/typing/mode_intf.mli
+++ b/ocaml/typing/mode_intf.mli
@@ -447,11 +447,6 @@ module type S = sig
   val value_to_alloc_r2g : ('l * 'r) Value.t -> ('l * 'r) Alloc.t
 
   module Modality : sig
-    (* CR zqian: have [const] and [var], and an injection from [const] to [var]. *)
-    type _user = private User
-
-    type _internal = private Internal
-
     type ('m, 'a) raw =
       | Meet_with : 'a -> (('a, 'd) mode_comonadic, 'a) raw
           (** [Meet_with c] takes [x] and returns [meet c x]. [c] can be [max]
@@ -472,52 +467,49 @@ module type S = sig
     module Value : sig
       type atom := t
 
-      (** A modality that acts on [Value] modes. Conceptually it is a sequnce of
-          [atom] that acts on individual axes. *)
-      type 'd t
-
-      type user = _user t
-
-      type internal = _internal t
-
-      (** Internalize a modality. *)
-      val internalize : 'd t -> internal
-
-      (** The identity modality. *)
-      val id : user
+      type error =
+        | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error
 
-      (** Same as [id] but internalized for convenience. *)
-      val id' : internal
+      type nonrec equate_error = equate_step * error
 
-      (** The undefined modality. *)
-      val undefined : internal
+      module Const : sig
+        (** A modality that acts on [Value] modes. Conceptually it is a sequnce
+            of [atom] that acts on individual axes. *)
+        type t
 
-      (** Apply a user modality on mode. *)
-      val apply_user : user -> ('l * 'r) Value.t -> ('l * 'r) Value.t
+        (** The identity modality. *)
+        val id : t
 
-      (** Apply a modality on a left mode. *)
-      val apply_left : 'd t -> (allowed * 'r) Value.t -> Value.l
+        (** Apply a modality on mode. *)
+        val apply : t -> ('l * 'r) Value.t -> ('l * 'r) Value.t
 
-      (* CR zqian: call this [compose]. *)
+        (** [compose m t] returns the modality that is [m] after [t]. *)
+        val compose : atom -> t -> t
 
-      (* CR zqian: call this [compose]. *)
+        (** [singleton m] returns the modality containing only [m]. *)
+        val singleton : atom -> t
 
-      (** [cons m t] returns the modality that is [m] after [t]. *)
-      val cons : atom -> user -> user
+        (** Returns the list of [atom] in the given modality. The list is
+            commutative. *)
+        val to_list : t -> atom list
 
-      (** [singleton m] returns the modality containing only [m]. *)
-      val singleton : atom -> user
+        (** [equate t0 t1] checks that [t0 = t1].
+            Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *)
+        val equate : t -> t -> (unit, equate_error) Result.t
+      end
 
-      (* CR zqian: return record, then we don't need [Exist.t]. *)
+      (** A modality that acts on [Value] modes. Conceptually it is a sequnce of
+          [atom] that acts on individual axes. *)
+      type t
 
-      (* CR zqian: return record, then we don't need [Exist.t]. *)
+      (** The identity modality. *)
+      val id : t
 
-      (** Returns the list of [atom] in the given modality. The list is
-          commutative. *)
-      val to_list : user -> atom list
+      (** The undefined modality. *)
+      val undefined : t
 
-      type error =
-        | Error : ('m, 'a, _) Value.axis * ('m, 'a) raw Solver.error -> error
+      (** Apply a modality on a left mode. *)
+      val apply : t -> (allowed * 'r) Value.t -> Value.l
 
       (** [sub t0 t1] checks that [t0 <= t1].
           Definition: [t0 <= t1] iff [forall a. t0(a) <= t1(a)].
@@ -526,19 +518,17 @@ module type S = sig
           [ax] is the axis on which the modalities disagree. [left] is the
           projection of [t0] on [ax], and [right] is the projection of [t1] on
           [ax]. *)
-      val sub : 'd t -> 'd t -> (unit, error) Result.t
-
-      type nonrec equate_error = equate_step * error
+      val sub : t -> t -> (unit, error) Result.t
 
       (** [equate t0 t1] checks that [t0 = t1].
           Definition: [t0 = t1] iff [t0 <= t1] and [t1 <= t0]. *)
-      val equate : 'd t -> 'd t -> (unit, equate_error) Result.t
+      val equate : t -> t -> (unit, equate_error) Result.t
 
       (** Printing for debugging. *)
-      val print : Format.formatter -> 'd t -> unit
+      val print : Format.formatter -> t -> unit
 
       (* CR zqian: consider spliting the [lr]. *)
-      val infer : md_mode:Value.lr -> mode:Value.l -> internal
+      val infer : md_mode:Value.lr -> mode:Value.l -> t
 
       (** Returns a user modality weaker than the given modality. The returned
       modality will be pushed to identity modality if possible. The given
@@ -550,18 +540,17 @@ module type S = sig
       - [let m' = zap_to_id m in (...; sub m m')] always succeeds, where [...]
         might mutate [m].
       *)
-      val zap_to_id : 'd t -> user
-
-      (* CR zqian: rename to [to_const_exn]. *)
-
-      (* CR zqian: rename to [to_const_exn]. *)
+      val zap_to_id : t -> Const.t
 
       (** Returns a user modality by asserting the given modality is already
       user modality and returning it. *)
-      val zap_assert : 'd t -> user
+      val to_const_exn : t -> Const.t
+
+      (** Convert a const modality. *)
+      val of_const : Const.t -> t
 
       (** The top modality; [sub x max] succeeds for any [x]. *)
-      val max : user
+      val max : t
     end
   end
 end
diff --git a/ocaml/typing/predef.ml b/ocaml/typing/predef.ml
index 2cf6568dd24..e3586e74f08 100644
--- a/ocaml/typing/predef.ml
+++ b/ocaml/typing/predef.ml
@@ -294,7 +294,7 @@ let build_initial_env add_type add_extension empty_env =
               (fun x ->
                 {
                   ca_type=x;
-                  ca_modalities=Mode.Modality.Value.id;
+                  ca_modalities=Mode.Modality.Value.Const.id;
                   ca_loc=Location.none
                 })
               args);
@@ -312,7 +312,7 @@ let build_initial_env add_type add_extension empty_env =
   in
   let variant constrs jkinds = Type_variant (constrs, Variant_boxed jkinds) in
   let unrestricted tvar =
-    {ca_type=tvar; ca_modalities=Mode.Modality.Value.id; ca_loc=Location.none}
+    {ca_type=tvar; ca_modalities=Mode.Modality.Value.Const.id; ca_loc=Location.none}
   in
   empty_env
   (* Predefined types *)
@@ -374,7 +374,7 @@ let build_initial_env add_type add_extension empty_env =
              {
                ld_id=id;
                ld_mutable=Immutable;
-               ld_modalities=Mode.Modality.Value.id;
+               ld_modalities=Mode.Modality.Value.Const.id;
                ld_type=field_type;
                ld_jkind=jkind;
                ld_loc=Location.none;
diff --git a/ocaml/typing/printtyp.ml b/ocaml/typing/printtyp.ml
index 8d45c5497e5..abea6d7d256 100644
--- a/ocaml/typing/printtyp.ml
+++ b/ocaml/typing/printtyp.ml
@@ -1292,7 +1292,7 @@ let tree_of_modality (t : Mode.Modality.t) =
   | _ -> Option.map (fun x -> Ogf_new x) (tree_of_modality_new t)
 
 let tree_of_modalities mutability t =
-  let l = Mode.Modality.Value.to_list t in
+  let l = Mode.Modality.Value.Const.to_list t in
   (* CR zqian: decouple mutable and modalities *)
   let l =
     if Types.is_mutable mutability then
@@ -1303,7 +1303,7 @@ let tree_of_modalities mutability t =
   List.filter_map tree_of_modality l
 
 let tree_of_modalities_new t =
-  let l = Mode.Modality.Value.to_list t in
+  let l = Mode.Modality.Value.Const.to_list t in
   List.filter_map tree_of_modality_new l
 
 (** [tree_of_mode m l] finds the outcome node in [l] that corresponds to [m].
diff --git a/ocaml/typing/typeclass.ml b/ocaml/typing/typeclass.ml
index b5ab3774163..69f843c079f 100644
--- a/ocaml/typing/typeclass.ml
+++ b/ocaml/typing/typeclass.ml
@@ -488,7 +488,7 @@ let enter_ancestor_met ~loc name ~sign ~meths ~cl_num ~ty ~attrs met_env =
   let check s = Warnings.Unused_ancestor s in
   let kind = Val_anc (sign, meths, cl_num) in
   let desc =
-    { val_type = ty; val_modalities = Modality.Value.id'; val_kind = kind;
+    { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind;
       val_attributes = attrs;
       val_zero_alloc = Builtin_attributes.Default_zero_alloc;
       Types.val_loc = loc;
@@ -504,7 +504,7 @@ let add_self_met loc id sign self_var_kind vars cl_num
   in
   let kind = Val_self (sign, self_var_kind, vars, cl_num) in
   let desc =
-    { val_type = ty; val_modalities = Modality.Value.id'; val_kind = kind;
+    { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind;
       val_attributes = attrs;
       val_zero_alloc = Builtin_attributes.Default_zero_alloc;
       Types.val_loc = loc;
@@ -520,7 +520,7 @@ let add_instance_var_met loc label id sign cl_num attrs met_env =
   in
   let kind = Val_ivar (mut, cl_num) in
   let desc =
-    { val_type = ty; val_modalities = Modality.Value.id'; val_kind = kind;
+    { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind;
       val_attributes = attrs;
       Types.val_loc = loc;
       val_zero_alloc = Builtin_attributes.Default_zero_alloc;
@@ -1464,7 +1464,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
              in
              let desc =
                {val_type = expr.exp_type;
-                val_modalities = Modality.Value.id';
+                val_modalities = Modality.Value.id;
                 val_kind = Val_ivar (Immutable, cl_num);
                 val_attributes = [];
                 val_zero_alloc = Builtin_attributes.Default_zero_alloc;
diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml
index 2ef222a76e7..1042cc84d6f 100644
--- a/ocaml/typing/typecore.ml
+++ b/ocaml/typing/typecore.ml
@@ -447,7 +447,7 @@ let mode_legacy = mode_default Value.legacy
 
 let mode_modality modality expected_mode =
   expected_mode.mode
-  |> Modality.Value.apply_user modality
+  |> Modality.Value.Const.apply modality
   |> mode_default
 
 (* used when entering a function;
@@ -1131,7 +1131,7 @@ let add_pattern_variables ?check ?check_as env pv =
        let check = if pv_as_var then check_as else check in
        Env.add_value ?check ~mode:pv_mode pv_id
          {val_type = pv_type; val_kind = Val_reg; Types.val_loc = pv_loc;
-          val_attributes = pv_attributes; val_modalities = Modality.Value.id |> Modality.Value.internalize;
+          val_attributes = pv_attributes; val_modalities = Modality.Value.id;
           val_zero_alloc = Builtin_attributes.Default_zero_alloc;
           val_uid = pv_uid
          } env
@@ -2433,10 +2433,10 @@ and type_pat_aux
     let ty_elt, arg_sort = solve_Ppat_array ~refine loc env mutability expected_ty in
     let modalities =
       if Types.is_mutable mutability then Typemode.mutable_implied_modalities
-      else Modality.Value.id
+      else Modality.Value.Const.id
     in
     check_project_mutability ~loc ~env:!env mutability alloc_mode.mode;
-    let alloc_mode = Modality.Value.apply_user modalities alloc_mode.mode in
+    let alloc_mode = Modality.Value.Const.apply modalities alloc_mode.mode in
     let alloc_mode = simple_pat_mode alloc_mode in
     let pl = List.map (fun p -> type_pat ~alloc_mode tps Value p ty_elt) spl in
     rvp {
@@ -2679,7 +2679,7 @@ and type_pat_aux
       let args =
         List.map2
           (fun p (ty, gf) ->
-             let alloc_mode = Modality.Value.apply_user gf alloc_mode.mode in
+             let alloc_mode = Modality.Value.Const.apply gf alloc_mode.mode in
              let alloc_mode = simple_pat_mode alloc_mode in
              type_pat ~alloc_mode tps Value p ty)
           sargs (List.combine ty_args_ty ty_args_gf)
@@ -2723,7 +2723,7 @@ and type_pat_aux
         let ty_arg =
           solve_Ppat_record_field ~refine loc env label label_lid record_ty in
         check_project_mutability ~loc ~env:!env label.lbl_mut alloc_mode.mode;
-        let mode = Modality.Value.apply_user label.lbl_modalities alloc_mode.mode in
+        let mode = Modality.Value.Const.apply label.lbl_modalities alloc_mode.mode in
         let alloc_mode = simple_pat_mode mode in
         (label_lid, label, type_pat tps Value ~alloc_mode sarg ty_arg)
       in
@@ -2926,7 +2926,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat =
             ; val_kind = Val_reg
             ; val_attributes = pv_attributes
             ; val_zero_alloc = Builtin_attributes.Default_zero_alloc
-            ; val_modalities = Modality.Value.id |> Modality.Value.internalize
+            ; val_modalities = Modality.Value.id
             ; val_loc = pv_loc
             ; val_uid = pv_uid
             }
@@ -2938,7 +2938,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat =
             ; val_kind = Val_ivar (Immutable, cl_num)
             ; val_attributes = pv_attributes
             ; val_zero_alloc = Builtin_attributes.Default_zero_alloc
-            ; val_modalities = Modality.Value.id |> Modality.Value.internalize
+            ; val_modalities = Modality.Value.id
             ; val_loc = pv_loc
             ; val_uid = pv_uid
             }
@@ -5733,7 +5733,7 @@ and type_expect_
                   with_explanation (fun () ->
                     unify_exp_types loc env (instance ty_expected) ty_res2);
                   check_project_mutability ~loc:exp.exp_loc ~env lbl.lbl_mut mode;
-                  let mode = Modality.Value.apply_user lbl.lbl_modalities mode in
+                  let mode = Modality.Value.Const.apply lbl.lbl_modalities mode in
                   check_construct_mutability ~loc ~env lbl.lbl_mut argument_mode;
                   let argument_mode =
                     mode_modality lbl.lbl_modalities argument_mode
@@ -5784,7 +5784,7 @@ and type_expect_
         end ~post:generalize_structure
       in
       check_project_mutability ~loc:record.exp_loc ~env label.lbl_mut rmode;
-      let mode = Modality.Value.apply_user label.lbl_modalities rmode in
+      let mode = Modality.Value.Const.apply label.lbl_modalities rmode in
       let boxing : texp_field_boxing =
         let is_float_boxing =
           match label.lbl_repres with
@@ -7471,7 +7471,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
           { val_type = ty; val_kind = Val_reg;
             val_attributes = [];
             val_zero_alloc = Builtin_attributes.Default_zero_alloc;
-            val_modalities = Modality.Value.id |> Modality.Value.internalize;
+            val_modalities = Modality.Value.id;
             val_loc = Location.none;
             val_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
           }
@@ -8767,7 +8767,7 @@ and type_generic_array
     if Types.is_mutable mutability then
       Predef.type_array, Typemode.mutable_implied_modalities
     else
-      Predef.type_iarray, Modality.Value.id
+      Predef.type_iarray, Modality.Value.Const.id
   in
   check_construct_mutability ~loc ~env mutability argument_mode;
   let argument_mode = mode_modality modalities argument_mode in
diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml
index c19a838a114..23a381bd20d 100644
--- a/ocaml/typing/typedecl.ml
+++ b/ocaml/typing/typedecl.ml
@@ -2876,7 +2876,7 @@ let transl_value_decl env loc valdecl =
       let modalities =
         valdecl.pval_modalities
         |> Typemode.transl_modalities Immutable
-        |> Mode.Modality.Value.internalize
+        |> Mode.Modality.Value.of_const
       in
       let default_arity =
         let rec count_arrows n ty =
@@ -2910,7 +2910,7 @@ let transl_value_decl env loc valdecl =
   | _ ->
       let modalities =
         match valdecl.pval_modalities with
-        | [] -> Mode.Modality.Value.id'
+        | [] -> Mode.Modality.Value.id
         | m :: _ -> raise (Error(m.loc, Modality_on_primitive))
       in
       let global_repr =
diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml
index 23ffb58aee7..0fb29498b0c 100644
--- a/ocaml/typing/typedtree.ml
+++ b/ocaml/typing/typedtree.ml
@@ -685,7 +685,7 @@ and label_declaration =
      ld_name: string loc;
      ld_uid: Uid.t;
      ld_mutable: mutability;
-     ld_modalities: Modality.Value.user;
+     ld_modalities: Modality.Value.Const.t;
      ld_type: core_type;
      ld_loc: Location.t;
      ld_attributes: attribute list;
@@ -705,7 +705,7 @@ and constructor_declaration =
 
 and constructor_argument =
   {
-    ca_modalities: Modality.Value.user;
+    ca_modalities: Modality.Value.Const.t;
     ca_type: core_type;
     ca_loc: Location.t;
   }
diff --git a/ocaml/typing/typedtree.mli b/ocaml/typing/typedtree.mli
index a1479294def..6d9d8f4baf3 100644
--- a/ocaml/typing/typedtree.mli
+++ b/ocaml/typing/typedtree.mli
@@ -943,7 +943,7 @@ and label_declaration =
      ld_name: string loc;
      ld_uid: Uid.t;
      ld_mutable: Types.mutability;
-     ld_modalities: Mode.Modality.Value.user;
+     ld_modalities: Mode.Modality.Value.Const.t;
      ld_type: core_type;
      ld_loc: Location.t;
      ld_attributes: attributes;
@@ -963,7 +963,7 @@ and constructor_declaration =
 
 and constructor_argument =
   {
-    ca_modalities: Mode.Modality.Value.user;
+    ca_modalities: Mode.Modality.Value.Const.t;
     ca_type: core_type;
     ca_loc: Location.t;
   }
diff --git a/ocaml/typing/typemod.ml b/ocaml/typing/typemod.ml
index 29ffe0767fc..8a93df842d5 100644
--- a/ocaml/typing/typemod.ml
+++ b/ocaml/typing/typemod.ml
@@ -2119,13 +2119,12 @@ let remove_mode_and_jkind_variables env sg =
   let rm _env ty = Ctype.remove_mode_and_jkind_variables ty; None in
   List.find_map (nongen_signature_item env rm) sg |> ignore
 
-let rec map_inferred_modalities_sg : _ -> (Mode.Modality.Value.internal -> Mode.Modality.Value.user) -> _ -> _
-= fun env map sg ->
+let rec map_inferred_modalities_sg env map sg =
   let rec loop acc = function
     | Sig_value (id, desc, vis) :: rest ->
         let val_modalities =
           desc.val_modalities
-          |> map |> Mode.Modality.Value.internalize
+          |> map |> Mode.Modality.Value.of_const
         in
         let desc = {desc with val_modalities} in
         let item = Sig_value (id, desc, vis) in
@@ -2151,7 +2150,7 @@ and map_inferred_modalities_mty env map mty =
       match param with
       | Named (id, mty) ->
           let mty =
-            map_inferred_modalities_mty env Mode.Modality.Value.zap_assert mty
+            map_inferred_modalities_mty env Mode.Modality.Value.to_const_exn mty
           in
           Named (id, mty)
       | Unit -> Unit
@@ -2159,7 +2158,9 @@ and map_inferred_modalities_mty env map mty =
     let mty = map_inferred_modalities_mty env map mty in
     Mty_functor (param, mty)
   | Mty_strengthen (mty, path, alias) ->
-      let mty = map_inferred_modalities_mty env Mode.Modality.Value.zap_assert mty in
+      let mty = map_inferred_modalities_mty
+        env Mode.Modality.Value.to_const_exn mty
+      in
       Mty_strengthen (mty, path, alias)
 
 (* Helpers for typing recursive modules *)
diff --git a/ocaml/typing/typemode.ml b/ocaml/typing/typemode.ml
index 9ffb8aa5cd6..cdaec5f368b 100644
--- a/ocaml/typing/typemode.ml
+++ b/ocaml/typing/typemode.ml
@@ -97,14 +97,15 @@ let untransl_modalities ~loc m : Parsetree.modality loc list =
     in
     { txt = Parsetree.Modality s; loc }
   in
-  Modality.Value.to_list m |> List.map untransl_atom
+  Modality.Value.Const.to_list m |> List.map untransl_atom
 
 let compose_modalities modalities =
   (* The ordering:
      type r = { x : string @@ foo bar hello }
      is interpreted as
      x = foo (bar (hello (r))) *)
-  List.fold_right Modality.Value.cons modalities Modality.Value.id
+  List.fold_right Modality.Value.Const.compose modalities
+    Modality.Value.Const.id
 
 let mutable_implied_modalities : Modality.t list =
   [ Atom (Comonadic Areality, Meet_with Regionality.Const.Global);
diff --git a/ocaml/typing/typemode.mli b/ocaml/typing/typemode.mli
index 20e50d9cbd7..e801ef572cd 100644
--- a/ocaml/typing/typemode.mli
+++ b/ocaml/typing/typemode.mli
@@ -9,13 +9,13 @@ val transl_alloc_mode : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.t
 val transl_modalities :
   Types.mutability ->
   Parsetree.modality Location.loc list ->
-  Mode.Modality.Value.user
+  Mode.Modality.Value.Const.t
 
 val untransl_modalities :
   loc:Location.t ->
-  Mode.Modality.Value.user ->
+  Mode.Modality.Value.Const.t ->
   Parsetree.modality Location.loc list
 
 val is_mutable_implied_modality : Mode.Modality.t -> bool
 
-val mutable_implied_modalities : Mode.Modality.Value.user
+val mutable_implied_modalities : Mode.Modality.Value.Const.t
diff --git a/ocaml/typing/types.ml b/ocaml/typing/types.ml
index 8f2ba41f8af..fd103ed8c4f 100644
--- a/ocaml/typing/types.ml
+++ b/ocaml/typing/types.ml
@@ -318,7 +318,7 @@ and label_declaration =
   {
     ld_id: Ident.t;
     ld_mutable: mutability;
-    ld_modalities: Mode.Modality.Value.user;
+    ld_modalities: Mode.Modality.Value.Const.t;
     ld_type: type_expr;
     ld_jkind : jkind;
     ld_loc: Location.t;
@@ -338,7 +338,7 @@ and constructor_declaration =
 
 and constructor_argument =
   {
-    ca_modalities: Mode.Modality.Value.user;
+    ca_modalities: Mode.Modality.Value.Const.t;
     ca_type: type_expr;
     ca_loc: Location.t;
   }
@@ -438,7 +438,7 @@ module type Wrapped = sig
 
   type value_description =
     { val_type: type_expr wrapped;                (* Type of the value *)
-      val_modalities : Mode.Modality.Value.internal;    (* Modalities on the value *)
+      val_modalities : Mode.Modality.Value.t;    (* Modalities on the value *)
       val_kind: value_kind;
       val_loc: Location.t;
       val_zero_alloc: Builtin_attributes.zero_alloc_attribute;
@@ -701,7 +701,7 @@ type label_description =
     lbl_res: type_expr;                 (* Type of the result *)
     lbl_arg: type_expr;                 (* Type of the argument *)
     lbl_mut: mutability;                (* Is this a mutable field? *)
-    lbl_modalities: Mode.Modality.Value.user;(* Is this a global field? *)
+    lbl_modalities: Mode.Modality.Value.Const.t;(* Is this a global field? *)
     lbl_jkind : jkind;                (* Jkind of the argument *)
     lbl_pos: int;                       (* Position in block *)
     lbl_num: int;                       (* Position in type *)
diff --git a/ocaml/typing/types.mli b/ocaml/typing/types.mli
index bd3bbdceae9..0f9992b08ea 100644
--- a/ocaml/typing/types.mli
+++ b/ocaml/typing/types.mli
@@ -622,7 +622,7 @@ and label_declaration =
   {
     ld_id: Ident.t;
     ld_mutable: mutability;
-    ld_modalities: Mode.Modality.Value.user;
+    ld_modalities: Mode.Modality.Value.Const.t;
     ld_type: type_expr;
     ld_jkind : jkind;
     ld_loc: Location.t;
@@ -642,7 +642,7 @@ and constructor_declaration =
 
 and constructor_argument =
   {
-    ca_modalities: Mode.Modality.Value.user;
+    ca_modalities: Mode.Modality.Value.Const.t;
     ca_type: type_expr;
     ca_loc: Location.t;
   }
@@ -743,7 +743,7 @@ module type Wrapped = sig
 
   type value_description =
     { val_type: type_expr wrapped;                (* Type of the value *)
-      val_modalities: Mode.Modality.Value.internal;     (* Modalities on the value *)
+      val_modalities: Mode.Modality.Value.t;     (* Modalities on the value *)
       val_kind: value_kind;
       val_loc: Location.t;
       val_zero_alloc: Builtin_attributes.zero_alloc_attribute;
@@ -866,7 +866,7 @@ type label_description =
     lbl_res: type_expr;                 (* Type of the result *)
     lbl_arg: type_expr;                 (* Type of the argument *)
     lbl_mut: mutability;                (* Is this a mutable field? *)
-    lbl_modalities: Mode.Modality.Value.user;
+    lbl_modalities: Mode.Modality.Value.Const.t;
     (* Modalities on the field *)
     lbl_jkind : jkind;                (* Jkind of the argument *)
     lbl_pos: int;                       (* Position in block *)
diff --git a/ocaml/typing/uniqueness_analysis.ml b/ocaml/typing/uniqueness_analysis.ml
index 9d8c3dad226..5df9ac1853d 100644
--- a/ocaml/typing/uniqueness_analysis.ml
+++ b/ocaml/typing/uniqueness_analysis.ml
@@ -739,18 +739,18 @@ module Paths : sig
 
   (** [modal_child gf proj t] is [child prof t] when [gf] is [Unrestricted]
       and is [untracked] otherwise. *)
-  val modal_child : Modality.Value.user -> Projection.t -> t -> t
+  val modal_child : Modality.Value.Const.t -> Projection.t -> t -> t
 
   (** [tuple_field i t] is [child (Projection.Tuple_field i) t]. *)
   val tuple_field : int -> t -> t
 
   (** [record_field gf s t] is
       [modal_child gf (Projection.Record_field s) t]. *)
-  val record_field : Modality.Value.user -> string -> t -> t
+  val record_field : Modality.Value.Const.t -> string -> t -> t
 
   (** [construct_field gf s i t] is
       [modal_child gf (Projection.Construct_field(s, i)) t]. *)
-  val construct_field : Modality.Value.user -> string -> int -> t -> t
+  val construct_field : Modality.Value.Const.t -> string -> int -> t -> t
 
   (** [variant_field s t] is [child (Projection.Variant_field s) t]. *)
   val variant_field : string -> t -> t
@@ -780,7 +780,7 @@ end = struct
   let modal_child gf 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.to_list gf in
+    let gf = Modality.Value.Const.to_list gf in
     let l =
       List.filter
         (function
@@ -850,7 +850,7 @@ module Value : sig
       implicit record field values for kept fields in a [{ foo with ... }]
       expression. *)
   val implicit_record_field :
-    Modality.Value.user -> string -> t -> unique_use -> t
+    Modality.Value.Const.t -> string -> t -> unique_use -> t
 
   (** Mark the value as shared_or_unique   *)
   val mark_maybe_unique : t -> UF.t