diff --git a/typing/jkind.ml b/typing/jkind.ml
index 2fb09cc917..b351ba9056 100644
--- a/typing/jkind.ml
+++ b/typing/jkind.ml
@@ -1205,10 +1205,10 @@ module Jkind_desc = struct
     in
     let upper_bounds = to_.upper_bounds in
     let upper_bounds, added1 =
-      add_crossing ~axis:(Modal Portability) upper_bounds
+      add_crossing ~axis:(Modal (Comonadic Portability)) upper_bounds
     in
     let upper_bounds, added2 =
-      add_crossing ~axis:(Modal Contention) upper_bounds
+      add_crossing ~axis:(Modal (Monadic Contention)) upper_bounds
     in
     { to_ with upper_bounds }, added1 || added2
 
@@ -1606,19 +1606,19 @@ let extract_layout jk = jk.jkind.layout
 let get_modal_upper_bounds ~type_equal ~jkind_of_type jk : Alloc.Const.t =
   let bounds = jk.jkind.upper_bounds in
   { areality =
-      Bound.reduce ~axis:(Modal Locality) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Comonadic Areality)) ~type_equal ~jkind_of_type
         bounds.locality;
     linearity =
-      Bound.reduce ~axis:(Modal Linearity) ~type_equal ~jkind_of_type
-        bounds.linearity;
+      Bound.reduce ~axis:(Modal (Comonadic Linearity)) ~type_equal
+        ~jkind_of_type bounds.linearity;
     uniqueness =
-      Bound.reduce ~axis:(Modal Uniqueness) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Monadic Uniqueness)) ~type_equal ~jkind_of_type
         bounds.uniqueness;
     portability =
-      Bound.reduce ~axis:(Modal Portability) ~type_equal ~jkind_of_type
-        bounds.portability;
+      Bound.reduce ~axis:(Modal (Comonadic Portability)) ~type_equal
+        ~jkind_of_type bounds.portability;
     contention =
-      Bound.reduce ~axis:(Modal Contention) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Monadic Contention)) ~type_equal ~jkind_of_type
         bounds.contention
   }
 
diff --git a/typing/jkind_axis.ml b/typing/jkind_axis.ml
index 44b24a7b0f..2cba23b7f6 100644
--- a/typing/jkind_axis.ml
+++ b/typing/jkind_axis.ml
@@ -115,15 +115,6 @@ module Nullability = struct
 end
 
 module Axis = struct
-  module Modal = struct
-    type 'a t =
-      | Locality : Mode.Locality.Const.t t
-      | Linearity : Mode.Linearity.Const.t t
-      | Uniqueness : Mode.Uniqueness.Const.t t
-      | Portability : Mode.Portability.Const.t t
-      | Contention : Mode.Contention.Const.t t
-  end
-
   module Nonmodal = struct
     type 'a t =
       | Externality : Externality.t t
@@ -131,114 +122,67 @@ module Axis = struct
   end
 
   type 'a t =
-    | Modal of 'a Modal.t
-    | Nonmodal of 'a Nonmodal.t
+    | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
+    | Nonmodal : 'a Nonmodal.t -> 'a t
 
   type packed = Pack : 'a t -> packed
 
-  module Accent_lattice (M : Mode_intf.Lattice) : Axis_ops with type t = M.t =
-  struct
+  module Accent_lattice (M : Mode_intf.Lattice) = struct
     (* A functor to add some convenient functions to modal axes *)
     include M
 
-    let less_or_equal a b = Misc.Le_result.less_or_equal ~le a b
+    let less_or_equal a b : Misc.Le_result.t =
+      match le a b, le b a with
+      | true, true -> Equal
+      | true, false -> Less
+      | false, _ -> Not_le
 
-    let equal a b = Misc.Le_result.equal ~le a b
+    let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
   end
 
   let get (type a) : a t -> (module Axis_ops with type t = a) = function
-    | Modal Locality -> (module Accent_lattice (Mode.Locality.Const))
-    | Modal Linearity -> (module Accent_lattice (Mode.Linearity.Const))
-    | Modal Uniqueness -> (module Accent_lattice (Mode.Uniqueness.Const))
-    | Modal Portability -> (module Accent_lattice (Mode.Portability.Const))
-    | Modal Contention -> (module Accent_lattice (Mode.Contention.Const))
+    | Modal axis -> (module Accent_lattice (val Mode.Alloc.lattice_of_axis axis))
     | Nonmodal Externality -> (module Externality)
     | Nonmodal Nullability -> (module Nullability)
 
   let all =
-    [ Pack (Modal Locality);
-      Pack (Modal Uniqueness);
-      Pack (Modal Linearity);
-      Pack (Modal Contention);
-      Pack (Modal Portability);
+    [ Pack (Modal (Comonadic Areality));
+      Pack (Modal (Monadic Uniqueness));
+      Pack (Modal (Comonadic Linearity));
+      Pack (Modal (Monadic Contention));
+      Pack (Modal (Comonadic Portability));
       Pack (Nonmodal Externality);
       Pack (Nonmodal Nullability) ]
 
   let name (type a) : a t -> string = function
-    | Modal Locality -> "locality"
-    | Modal Linearity -> "linearity"
-    | Modal Uniqueness -> "uniqueness"
-    | Modal Portability -> "portability"
-    | Modal Contention -> "contention"
+    | Modal axis -> Format.asprintf "%a" Mode.Alloc.print_axis axis
     | Nonmodal Externality -> "externality"
     | Nonmodal Nullability -> "nullability"
 
   let is_modal (type a) : a t -> bool = function
-    | Modal Locality -> true
-    | Modal Linearity -> true
-    | Modal Uniqueness -> true
-    | Modal Portability -> true
-    | Modal Contention -> true
+    | Modal (Comonadic Areality) -> true
+    | Modal (Comonadic Linearity) -> true
+    | Modal (Monadic Uniqueness) -> true
+    | Modal (Comonadic Portability) -> true
+    | Modal (Monadic Contention) -> true
     | Nonmodal Externality -> true
     | Nonmodal Nullability -> false
 
-  (* CR aspsmith: This can get a lot simpler once we unify jkind axes with the axes in
-     Mode *)
-  let modality_is_const_for_axis (type a) (t : a t) modality =
+  let modality_is_const_for_axis (type a) (t : a t)
+      (modality : Mode.Modality.Value.Const.t) =
     match t with
     | Nonmodal Nullability | Nonmodal Externality -> false
     | Modal axis ->
-      let atoms = Mode.Modality.Value.Const.to_list modality in
-      List.exists
-        (fun (modality : Mode.Modality.t) ->
-          match axis, modality with
-          (* Constant modalities *)
-          | Locality, Atom (Comonadic Areality, Meet_with Global) -> true
-          | Linearity, Atom (Comonadic Linearity, Meet_with Many) -> true
-          | Uniqueness, Atom (Monadic Uniqueness, Join_with Aliased) -> true
-          | Portability, Atom (Comonadic Portability, Meet_with Portable) ->
-            true
-          | Contention, Atom (Monadic Contention, Join_with Contended) -> true
-          (* Modalities which are actually identity *)
-          | Locality, Atom (Comonadic Areality, Meet_with Local)
-          | Linearity, Atom (Comonadic Linearity, Meet_with Once)
-          | Uniqueness, Atom (Monadic Uniqueness, Join_with Unique)
-          | Portability, Atom (Comonadic Portability, Meet_with Nonportable)
-          | Contention, Atom (Monadic Contention, Join_with Uncontended) ->
-            false
-          (* Modalities which are neither constant nor identiy *)
-          | Locality, Atom (Comonadic Areality, Meet_with Regional)
-          | Contention, Atom (Monadic Contention, Join_with Shared) ->
-            Misc.fatal_error
-              "Don't yet know how to interpret non-constant, non-identity \
-               modalities"
-          (* Modalities which join or meet on an illegal axis *)
-          | _, Atom (Comonadic _, Join_with _) | _, Atom (Monadic _, Meet_with _)
-            ->
-            Misc.fatal_error "Illegal modality"
-          (* Mismatched axes *)
-          | Locality, Atom (Monadic Uniqueness, _)
-          | Locality, Atom (Monadic Contention, _)
-          | Locality, Atom (Comonadic Linearity, _)
-          | Locality, Atom (Comonadic Portability, _)
-          | Linearity, Atom (Comonadic Areality, _)
-          | Linearity, Atom (Monadic Uniqueness, _)
-          | Portability, Atom (Monadic Uniqueness, _)
-          | Contention, Atom (Monadic Uniqueness, _)
-          | Linearity, Atom (Comonadic Portability, _)
-          | Linearity, Atom (Monadic Contention, _)
-          | Uniqueness, Atom (Comonadic Areality, _)
-          | Uniqueness, Atom (Comonadic Linearity, _)
-          | Uniqueness, Atom (Comonadic Portability, _)
-          | Contention, Atom (Comonadic Areality, _)
-          | Contention, Atom (Comonadic Linearity, _)
-          | Contention, Atom (Comonadic Portability, _)
-          | Uniqueness, Atom (Monadic Contention, _)
-          | Portability, Atom (Comonadic Areality, _)
-          | Portability, Atom (Comonadic Linearity, _)
-          | Portability, Atom (Monadic Contention, _) ->
-            false)
-        atoms
+      let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
+      let modality = Mode.Modality.Value.Const.proj axis modality in
+      if Mode.Modality.is_constant modality
+      then true
+      else if Mode.Modality.is_id modality
+      then false
+      else
+        Misc.fatal_error
+          "Don't yet know how to interpret non-constant, non-identity \
+           modalities"
 end
 
 module type Axed = sig
@@ -259,21 +203,21 @@ module Axis_collection (T : Axed) = struct
 
   let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t =
     match axis with
-    | Modal Locality -> values.locality
-    | Modal Linearity -> values.linearity
-    | Modal Uniqueness -> values.uniqueness
-    | Modal Portability -> values.portability
-    | Modal Contention -> values.contention
+    | Modal (Comonadic Areality) -> values.locality
+    | Modal (Comonadic Linearity) -> values.linearity
+    | Modal (Monadic Uniqueness) -> values.uniqueness
+    | Modal (Comonadic Portability) -> values.portability
+    | Modal (Monadic Contention) -> values.contention
     | Nonmodal Externality -> values.externality
     | Nonmodal Nullability -> values.nullability
 
   let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) =
     match axis with
-    | Modal Locality -> { values with locality = value }
-    | Modal Linearity -> { values with linearity = value }
-    | Modal Uniqueness -> { values with uniqueness = value }
-    | Modal Portability -> { values with portability = value }
-    | Modal Contention -> { values with contention = value }
+    | Modal (Comonadic Areality) -> { values with locality = value }
+    | Modal (Comonadic Linearity) -> { values with linearity = value }
+    | Modal (Monadic Uniqueness) -> { values with uniqueness = value }
+    | Modal (Comonadic Portability) -> { values with portability = value }
+    | Modal (Monadic Contention) -> { values with contention = value }
     | Nonmodal Externality -> { values with externality = value }
     | Nonmodal Nullability -> { values with nullability = value }
 
@@ -287,11 +231,11 @@ module Axis_collection (T : Axed) = struct
 
       let[@inline] f { f } =
         let open M.Syntax in
-        let* locality = f ~axis:Axis.(Modal Locality) in
-        let* uniqueness = f ~axis:Axis.(Modal Uniqueness) in
-        let* linearity = f ~axis:Axis.(Modal Linearity) in
-        let* contention = f ~axis:Axis.(Modal Contention) in
-        let* portability = f ~axis:Axis.(Modal Portability) in
+        let* locality = f ~axis:Axis.(Modal (Comonadic Areality)) in
+        let* uniqueness = f ~axis:Axis.(Modal (Monadic Uniqueness)) in
+        let* linearity = f ~axis:Axis.(Modal (Comonadic Linearity)) in
+        let* contention = f ~axis:Axis.(Modal (Monadic Contention)) in
+        let* portability = f ~axis:Axis.(Modal (Comonadic Portability)) in
         let* externality = f ~axis:Axis.(Nonmodal Externality) in
         let* nullability = f ~axis:Axis.(Nonmodal Nullability) in
         M.return
@@ -380,11 +324,11 @@ module Axis_collection (T : Axed) = struct
           externality;
           nullability
         } ~combine =
-      combine (f ~axis:Axis.(Modal Locality) locality)
-      @@ combine (f ~axis:Axis.(Modal Uniqueness) uniqueness)
-      @@ combine (f ~axis:Axis.(Modal Linearity) linearity)
-      @@ combine (f ~axis:Axis.(Modal Contention) contention)
-      @@ combine (f ~axis:Axis.(Modal Portability) portability)
+      combine (f ~axis:Axis.(Modal (Comonadic Areality)) locality)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) linearity)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) contention)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) portability)
       @@ combine (f ~axis:Axis.(Nonmodal Externality) externality)
       @@ f ~axis:Axis.(Nonmodal Nullability) nullability
   end
@@ -417,11 +361,11 @@ module Axis_collection (T : Axed) = struct
           externality = ext2;
           nullability = nul2
         } ~combine =
-      combine (f ~axis:Axis.(Modal Locality) loc1 loc2)
-      @@ combine (f ~axis:Axis.(Modal Uniqueness) uni1 uni2)
-      @@ combine (f ~axis:Axis.(Modal Linearity) lin1 lin2)
-      @@ combine (f ~axis:Axis.(Modal Contention) con1 con2)
-      @@ combine (f ~axis:Axis.(Modal Portability) por1 por2)
+      combine (f ~axis:Axis.(Modal (Comonadic Areality)) loc1 loc2)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uni1 uni2)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) lin1 lin2)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) con1 con2)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) por1 por2)
       @@ combine (f ~axis:Axis.(Nonmodal Externality) ext1 ext2)
       @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2
   end
diff --git a/typing/jkind_axis.mli b/typing/jkind_axis.mli
index 16e54a95fc..e688322925 100644
--- a/typing/jkind_axis.mli
+++ b/typing/jkind_axis.mli
@@ -41,16 +41,6 @@ module Nullability : sig
 end
 
 module Axis : sig
-  (* CR zqian: remove this and use [Mode.Alloc.axis] instead *)
-  module Modal : sig
-    type 'a t =
-      | Locality : Mode.Locality.Const.t t
-      | Linearity : Mode.Linearity.Const.t t
-      | Uniqueness : Mode.Uniqueness.Const.t t
-      | Portability : Mode.Portability.Const.t t
-      | Contention : Mode.Contention.Const.t t
-  end
-
   module Nonmodal : sig
     type 'a t =
       | Externality : Externality.t t
@@ -59,8 +49,8 @@ module Axis : sig
 
   (** Represents an axis of a jkind *)
   type 'a t =
-    | Modal of 'a Modal.t
-    | Nonmodal of 'a Nonmodal.t
+    | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
+    | Nonmodal : 'a Nonmodal.t -> 'a t
 
   type packed = Pack : 'a t -> packed
 
diff --git a/typing/mode.ml b/typing/mode.ml
index 7a53755207..ac880d7447 100644
--- a/typing/mode.ml
+++ b/typing/mode.ml
@@ -547,7 +547,7 @@ module Lattices_mono = struct
 
     let print : type p r. _ -> (p, r) t -> unit =
      fun ppf -> function
-      | Areality -> Format.fprintf ppf "areality"
+      | Areality -> Format.fprintf ppf "locality"
       | Linearity -> Format.fprintf ppf "linearity"
       | Portability -> Format.fprintf ppf "portability"
       | Uniqueness -> Format.fprintf ppf "uniqueness"
@@ -1540,6 +1540,13 @@ module Comonadic_with (Areality : Areality) = struct
     let print_axis ax ppf a =
       let obj = proj_obj ax in
       C.print obj ppf a
+
+    let lattice_of_axis (type a) (axis : (t, a) Axis.t) :
+        (module Lattice with type t = a) =
+      match axis with
+      | Areality -> (module Areality.Const)
+      | Linearity -> (module Linearity.Const)
+      | Portability -> (module Portability.Const)
   end
 
   let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m
@@ -1633,6 +1640,12 @@ module Monadic = struct
     let le_axis ax a b =
       let obj = proj_obj ax in
       C.le obj b a
+
+    let lattice_of_axis (type a) (axis : (t, a) Axis.t) :
+        (module Lattice with type t = a) =
+      match axis with
+      | Uniqueness -> (module Uniqueness.Const)
+      | Contention -> (module Contention.Const)
   end
 
   let proj ax m = Solver.via_monotone (proj_obj ax) (Proj (Obj.obj, ax)) m
@@ -1709,6 +1722,19 @@ module Value_with (Areality : Areality) = struct
         (Comonadic.Const.t, 'a) Axis.t
         -> (('a, 'd) mode_comonadic, 'a, 'd) axis
 
+  type 'd axis_packed = P : ('m, 'a, 'd) axis -> 'd axis_packed
+
+  let print_axis (type m a d) ppf (axis : (m, a, d) axis) =
+    match axis with
+    | Monadic ax -> Axis.print ppf ax
+    | Comonadic ax -> Axis.print ppf ax
+
+  let lattice_of_axis (type m a d) (axis : (m, a, d) axis) :
+      (module Lattice with type t = a) =
+    match axis with
+    | Comonadic ax -> Comonadic.Const.lattice_of_axis ax
+    | Monadic ax -> Monadic.Const.lattice_of_axis ax
+
   let proj_obj : type m a d. (m, a, d) axis -> a C.obj = function
     | Monadic ax -> Monadic.proj_obj ax
     | Comonadic ax -> Comonadic.proj_obj ax
@@ -1886,6 +1912,12 @@ module Value_with (Areality : Areality) = struct
       | Comonadic ax -> Comonadic.max_axis ax
       | Monadic ax -> Monadic.max_axis ax
 
+    let is_max : type m a d. (m, a, d) axis -> a -> bool =
+     fun ax m -> le_axis ax (max_axis ax) m
+
+    let is_min : type m a d. (m, a, d) axis -> a -> bool =
+     fun ax m -> le_axis ax m (min_axis ax)
+
     let split = split
 
     let merge = merge
@@ -2144,6 +2176,16 @@ module Const = struct
     let areality = C.locality_as_regionality areality in
     { areality; linearity; portability; uniqueness; contention }
 
+  module Axis = struct
+    let alloc_as_value : type d. d Alloc.axis_packed -> d Value.axis_packed =
+      function
+      | P (Comonadic Areality) -> P (Comonadic Areality)
+      | P (Comonadic Linearity) -> P (Comonadic Linearity)
+      | P (Comonadic Portability) -> P (Comonadic Portability)
+      | P (Monadic Uniqueness) -> P (Monadic Uniqueness)
+      | P (Monadic Contention) -> P (Monadic Contention)
+  end
+
   let locality_as_regionality = C.locality_as_regionality
 end
 
@@ -2189,8 +2231,13 @@ module Modality = struct
 
   let is_id (Atom (ax, a)) =
     match a with
-    | Join_with c -> Value.Const.le_axis ax c (Value.Const.min_axis ax)
-    | Meet_with c -> Value.Const.le_axis ax (Value.Const.max_axis ax) c
+    | Join_with c -> Value.Const.is_min ax c
+    | Meet_with c -> Value.Const.is_max ax c
+
+  let is_constant (Atom (ax, a)) =
+    match a with
+    | Join_with c -> Value.Const.is_max ax c
+    | Meet_with c -> Value.Const.is_min ax c
 
   let print ppf = function
     | Atom (ax, Join_with c) ->
@@ -2249,6 +2296,9 @@ module Modality = struct
             (let ax : _ Axis.t = Contention in
              Atom (Monadic ax, Join_with (Axis.proj ax c))) ]
 
+      let proj ax = function
+        | Join_const c -> Atom (Monadic ax, Join_with (Axis.proj ax c))
+
       let print ppf = function
         | Join_const c -> Format.fprintf ppf "join_const(%a)" Mode.Const.print c
     end
@@ -2391,6 +2441,9 @@ module Modality = struct
             (let ax : _ Axis.t = Portability 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 print ppf = function
         | Meet_const c -> Format.fprintf ppf "meet_const(%a)" Mode.Const.print c
     end
@@ -2552,6 +2605,11 @@ module Modality = struct
 
       let to_list { monadic; comonadic } =
         Comonadic.to_list comonadic @ Monadic.to_list monadic
+
+      let proj (type m a d) (ax : (m, a, d) Value.axis) { monadic; comonadic } =
+        match ax with
+        | Monadic ax -> Monadic.proj ax monadic
+        | Comonadic ax -> Comonadic.proj ax comonadic
     end
 
     type t = (Monadic.t, Comonadic.t) monadic_comonadic
diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli
index 191d77e6a9..cde9c561f1 100644
--- a/typing/mode_intf.mli
+++ b/typing/mode_intf.mli
@@ -278,6 +278,8 @@ module type S = sig
       | Contention : (monadic, Contention.Const.t) t
 
     val print : Format.formatter -> ('p, 'r) t -> unit
+
+    val eq : ('p, 'r0) t -> ('p, 'r1) t -> ('r0, 'r1) Misc.eq option
   end
 
   module type Mode := sig
@@ -317,6 +319,12 @@ module type S = sig
           (Comonadic.Const.t, 'a) Axis.t
           -> (('a, 'd) mode_comonadic, 'a, 'd) axis
 
+    type 'd axis_packed = P : ('m, 'a, 'd) axis -> 'd axis_packed
+
+    val print_axis : Format.formatter -> ('m, 'a, 'd) axis -> unit
+
+    val lattice_of_axis : ('m, 'a, 'd) axis -> (module Lattice with type t = 'a)
+
     type ('a, 'b, 'c, 'd, 'e) modes =
       { areality : 'a;
         linearity : 'b;
@@ -432,6 +440,10 @@ module type S = sig
   module Const : sig
     val alloc_as_value : Alloc.Const.t -> Value.Const.t
 
+    module Axis : sig
+      val alloc_as_value : 'd Alloc.axis_packed -> 'd Value.axis_packed
+    end
+
     val locality_as_regionality : Locality.Const.t -> Regionality.Const.t
   end
 
@@ -471,6 +483,9 @@ module type S = sig
     (** Test if the given modality is the identity modality. *)
     val is_id : t -> bool
 
+    (** Test if the given modality is a constant modality. *)
+    val is_constant : t -> bool
+
     (** Printing for debugging *)
     val print : Format.formatter -> t -> unit
 
@@ -510,6 +525,9 @@ module type S = sig
             output list exactly once. *)
         val to_list : t -> atom list
 
+        (** Project out the [atom] for the given axis in the given modality. *)
+        val proj : ('m, 'a, 'd) Value.axis -> t -> atom
+
         (** [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
diff --git a/typing/typemode.ml b/typing/typemode.ml
index 03f14670d8..21eb120d5f 100644
--- a/typing/typemode.ml
+++ b/typing/typemode.ml
@@ -25,25 +25,32 @@ exception Error of Location.t * error
 
 module Axis_pair = struct
   type 'm t =
-    | Modal_axis_pair : 'a Axis.Modal.t * 'a -> modal t
+    | Modal_axis_pair : ('m, 'a, 'd) Mode.Alloc.axis * 'a -> modal t
     | Any_axis_pair : 'a Axis.t * 'a -> maybe_nonmodal t
 
   let of_string s =
     let open Mode in
     match s with
-    | "local" -> Any_axis_pair (Modal Locality, Locality.Const.Local)
-    | "global" -> Any_axis_pair (Modal Locality, Locality.Const.Global)
-    | "unique" -> Any_axis_pair (Modal Uniqueness, Uniqueness.Const.Unique)
-    | "aliased" -> Any_axis_pair (Modal Uniqueness, Uniqueness.Const.Aliased)
-    | "once" -> Any_axis_pair (Modal Linearity, Linearity.Const.Once)
-    | "many" -> Any_axis_pair (Modal Linearity, Linearity.Const.Many)
+    | "local" -> Any_axis_pair (Modal (Comonadic Areality), Locality.Const.Local)
+    | "global" ->
+      Any_axis_pair (Modal (Comonadic Areality), Locality.Const.Global)
+    | "unique" ->
+      Any_axis_pair (Modal (Monadic Uniqueness), Uniqueness.Const.Unique)
+    | "aliased" ->
+      Any_axis_pair (Modal (Monadic Uniqueness), Uniqueness.Const.Aliased)
+    | "once" -> Any_axis_pair (Modal (Comonadic Linearity), Linearity.Const.Once)
+    | "many" -> Any_axis_pair (Modal (Comonadic Linearity), Linearity.Const.Many)
     | "nonportable" ->
-      Any_axis_pair (Modal Portability, Portability.Const.Nonportable)
-    | "portable" -> Any_axis_pair (Modal Portability, Portability.Const.Portable)
-    | "contended" -> Any_axis_pair (Modal Contention, Contention.Const.Contended)
-    | "shared" -> Any_axis_pair (Modal Contention, Contention.Const.Shared)
+      Any_axis_pair
+        (Modal (Comonadic Portability), Portability.Const.Nonportable)
+    | "portable" ->
+      Any_axis_pair (Modal (Comonadic Portability), Portability.Const.Portable)
+    | "contended" ->
+      Any_axis_pair (Modal (Monadic Contention), Contention.Const.Contended)
+    | "shared" ->
+      Any_axis_pair (Modal (Monadic Contention), Contention.Const.Shared)
     | "uncontended" ->
-      Any_axis_pair (Modal Contention, Contention.Const.Uncontended)
+      Any_axis_pair (Modal (Monadic Contention), Contention.Const.Uncontended)
     | "maybe_null" ->
       Any_axis_pair (Nonmodal Nullability, Nullability.Maybe_null)
     | "non_null" -> Any_axis_pair (Nonmodal Nullability, Nullability.Non_null)
@@ -109,7 +116,9 @@ let transl_modifier_annots annots =
 
 let transl_mode_annots annots : Alloc.Const.Option.t =
   let step modifiers_so_far annot =
-    let { txt = Modal_axis_pair (type a) ((axis, mode) : a Axis.Modal.t * a);
+    let { txt =
+            Modal_axis_pair (type m a d)
+              ((axis, mode) : (m, a, d) Mode.Alloc.axis * a);
           loc
         } =
       transl_annot ~annot_type:Mode ~required_mode_maturity:(Some Stable)
@@ -156,16 +165,16 @@ let transl_modality ~maturity { txt = Parsetree.Modality modality; loc } =
       { txt = modality; loc }
   in
   match axis_pair.txt with
-  | Modal_axis_pair (Locality, mode) ->
+  | Modal_axis_pair (Comonadic Areality, mode) ->
     Modality.Atom
       (Comonadic Areality, Meet_with (Const.locality_as_regionality mode))
-  | Modal_axis_pair (Linearity, mode) ->
+  | Modal_axis_pair (Comonadic Linearity, mode) ->
     Modality.Atom (Comonadic Linearity, Meet_with mode)
-  | Modal_axis_pair (Uniqueness, mode) ->
-    Modality.Atom (Monadic Uniqueness, Join_with mode)
-  | Modal_axis_pair (Portability, mode) ->
+  | Modal_axis_pair (Comonadic Portability, mode) ->
     Modality.Atom (Comonadic Portability, Meet_with mode)
-  | Modal_axis_pair (Contention, mode) ->
+  | Modal_axis_pair (Monadic Uniqueness, mode) ->
+    Modality.Atom (Monadic Uniqueness, Join_with mode)
+  | Modal_axis_pair (Monadic Contention, mode) ->
     Modality.Atom (Monadic Contention, Join_with mode)
 
 let untransl_modality (a : Modality.t) : Parsetree.modality loc =