From 41f8829696e0919bb73661212f04a1fb319e9791 Mon Sep 17 00:00:00 2001
From: Aspen Smith <aspsmith@janestreet.com>
Date: Fri, 10 Jan 2025 14:11:59 -0500
Subject: [PATCH] Move (most of) the type definitions for jkind into Types

Jkinds are morally mutually recursive with types, since jkinds can contain
types (in the with-bounds) and types can be bounded on jkinds (eg for Tvar and
Tunivar). We previously "broke up" this recursion with a type parameter for
type_expr on the bits of Jkind.t that contain type_exprs, and by defining two
modules, Jkind_types and Jkind - the first with the type parameter, and the
second with the parameter instantiated to Types.type_expr. This has caused a lot
of headache and confusion, is hard to follow (you lose jump-to-definition, among
other things) and generally puts friction on algorithms for kinds that need to
do things with type_exprs (which we're about to do a lot more, for normalizing
of jkinds).

Instead, this commit starts the (multi-stage) process of splitting up jkind,
starting by just moving the type definitions (omitting sort and layout so far)
into types.ml, in the same recursive type declaration as type_expr. This
simplifies things a /lot/, without really losing much in terms of things being
broken up (the algorithms are still just defined in jkind.ml)!
---
 typing/jkind.ml        | 378 ++++++++++++++++++++++++++++++-----------
 typing/jkind.mli       | 186 ++++++++++----------
 typing/jkind_types.ml  | 259 ----------------------------
 typing/jkind_types.mli | 126 --------------
 typing/types.ml        |  50 +++++-
 typing/types.mli       |  60 ++++++-
 utils/misc.ml          |  18 ++
 utils/misc.mli         |  18 ++
 8 files changed, 511 insertions(+), 584 deletions(-)

diff --git a/typing/jkind.ml b/typing/jkind.ml
index 87c7c0ea7b4..61526480c63 100644
--- a/typing/jkind.ml
+++ b/typing/jkind.ml
@@ -15,6 +15,7 @@
 open Mode
 open Jkind_types
 open Jkind_axis
+open Types
 
 [@@@warning "+9"]
 
@@ -32,8 +33,6 @@ end
 
 type sort = Sort.t
 
-type type_expr = Types.type_expr
-
 (* A *layout* of a type describes the way values of that type are stored at
    runtime, including details like width, register convention, calling
    convention, etc. A layout may be *representable* or *unrepresentable*.  The
@@ -317,41 +316,6 @@ module History = struct
   let has_warned t = t.has_warned
 end
 
-(*********************************)
-(* Main type declarations *)
-
-type 'd t = (type_expr, 'd) Jkind_types.t
-
-type jkind_l = (allowed * disallowed) t
-
-type packed = Pack : 'd t -> packed [@@unboxed]
-
-include Allowance.Magic_allow_disallow (struct
-  type (_, _, 'd) sided = 'd t
-
-  let disallow_right t =
-    { t with jkind = Layout_and_axes.disallow_right t.jkind }
-
-  let disallow_left t = { t with jkind = Layout_and_axes.disallow_left t.jkind }
-
-  let allow_right t = { t with jkind = Layout_and_axes.allow_right t.jkind }
-
-  let allow_left t = { t with jkind = Layout_and_axes.allow_left t.jkind }
-end)
-
-let try_allow_r t =
-  Option.map
-    (fun jkind -> { t with jkind })
-    (Layout_and_axes.try_allow_r t.jkind)
-
-let fresh_jkind jkind ~annotation ~why =
-  { jkind; annotation; history = Creation why; has_warned = false }
-  |> allow_left |> allow_right
-
-(* This version propagates the allowances from the [jkind] to the output. *)
-let fresh_jkind_poly jkind ~annotation ~why =
-  { jkind; annotation; history = Creation why; has_warned = false }
-
 (******************************)
 (*** user errors ***)
 
@@ -379,9 +343,123 @@ let raise ~loc err = raise (Error.User_error (loc, err))
 (*** Bounds, specialized to the real [type_expr] ***)
 
 module With_bounds = struct
-  include Jkind_types.With_bounds
+  type 'd t = 'd Types.with_bounds
+    constraint 'd = 'l * 'r
+
+  module Type_info = struct
+    type t = Types.with_bounds_type
+
+    let print ~print_type_expr ppf Types.{ type_expr; modality; nullability } =
+      let open Format in
+      if Mode.Modality.Value.Const.is_id modality
+      then print_type_expr ppf type_expr
+      else begin
+        fprintf ppf "(@[%a@ @@@@ %a%a])" print_type_expr type_expr
+          Mode.Modality.Value.Const.print modality
+          (fun ppf nullable -> if nullable then fprintf ppf "nullable")
+          nullability
+      end
+
+    let map_type_expr f (Types.{ type_expr; _ } as t) =
+      { t with type_expr = f type_expr }
+
+    let is_on_axis (type a) ~(axis : a Jkind_axis.Axis.t) (t : t) =
+      match axis with
+      | Nonmodal Externality -> true (* All fields matter for externality *)
+      | Nonmodal Nullability -> t.nullability
+      | Modal axis ->
+        let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
+        not
+          (Mode.Modality.Value.Const.proj axis t.modality
+          |> Mode.Modality.is_constant)
+
+    let compose_modality (t : t) ~then_ =
+      let modality = Mode.Modality.Value.Const.compose t.modality ~then_ in
+      assert (not (Mode.Modality.Value.Const.is_id modality));
+      { t with modality }
+
+    let create ~type_expr ~modality ~deep_only : t =
+      { type_expr; modality; nullability = not deep_only }
+  end
+
+  let to_list : type l r. (l * r) t -> _ = function
+    | No_with_bounds -> []
+    | With_bounds tys -> Misc.Nonempty_list.to_list tys
+
+  open Allowance
+
+  include Magic_allow_disallow (struct
+    type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r
+
+    let disallow_left :
+        type l r. (l * r) t -> (disallowed * r) t =
+      function
+      | No_with_bounds -> No_with_bounds
+      | With_bounds _ as b -> b
+
+    let disallow_right :
+        type l r. (l * r) t -> (l * disallowed) t =
+      function
+      | No_with_bounds -> No_with_bounds
+      | With_bounds _ as b -> b
+
+    let allow_left :
+        type l r. (allowed * r) t -> (l * r) t =
+      function
+      | No_with_bounds -> No_with_bounds
+      | With_bounds _ as b -> b
+
+    let allow_right :
+        type l r. (l * allowed) t -> (l * r) t =
+      function
+      | No_with_bounds -> No_with_bounds
+  end)
+
+  let try_allow_l :
+      type l r. (l * r) t -> (allowed * r) t option =
+    function
+    | No_with_bounds -> Some No_with_bounds
+    | With_bounds _ as b -> Some b
+
+  let try_allow_r :
+      type l r. (l * r) t -> (l * allowed) t option =
+    function
+    | No_with_bounds -> Some No_with_bounds
+    | With_bounds _ -> None
+
+  let map_type_expr (type l r) f :
+      (l * r) t -> (l * r) t = function
+    | No_with_bounds -> No_with_bounds
+    | With_bounds tys ->
+      With_bounds (Misc.Nonempty_list.map (Type_info.map_type_expr f) tys)
+
+  let types_on_axis (type l r a) ~(axis : a Jkind_axis.Axis.t) :
+      (l * r) t -> _ = function
+    | No_with_bounds -> []
+    | With_bounds (ti :: tis) ->
+      List.filter_map
+        (fun (type_info : Type_info.t) ->
+          if Type_info.is_on_axis ~axis type_info
+          then Some type_info.type_expr
+          else None)
+        (ti :: tis)
+
+  let compose_modality (type l r) ~then_ : (l * r) t -> (l * r) t =
+    function
+    | No_with_bounds -> No_with_bounds
+    | With_bounds ts ->
+      With_bounds (Misc.Nonempty_list.map (Type_info.compose_modality ~then_) ts)
 
-  type nonrec 'd t = (type_expr, 'd) t
+  let debug_print (type l r) ~print_type_expr ppf : (l * r) t -> _ =
+    let open Format in
+    function
+    | No_with_bounds -> fprintf ppf "No_with_bounds"
+    | With_bounds tys ->
+      fprintf ppf "With_bounds @[[%a]@]"
+        (Misc.Nonempty_list.pp_print
+           ~pp_sep:(fun ppf () -> fprintf ppf ";@ ")
+           (Type_info.print ~print_type_expr))
+        tys
 
   (* You might think that we can only do joins on the left. But that's not true!
      We can join constants. The important thing is that the allowances of both
@@ -393,9 +471,10 @@ module With_bounds = struct
     match bag1, bag2 with
     | No_with_bounds, No_with_bounds -> No_with_bounds
     | No_with_bounds, b -> b
-    | b, No_with_bounds -> b (* CR layouts v2.8: List concatentation is slow. *)
-    | With_bounds (ty1, tys1), With_bounds (ty2, tys2) ->
-      With_bounds (ty1, tys1 @ (ty2 :: tys2))
+    | b, No_with_bounds -> b
+    | With_bounds tys1, With_bounds tys2 ->
+      (* CR layouts v2.8: List concatentation is slow. *)
+      With_bounds (Misc.Nonempty_list.(tys1 @ tys2))
 
   let meet (type l1 l2) (bag1 : (l1 * allowed) t) (bag2 : (l2 * allowed) t) :
       (l1 * allowed) t =
@@ -405,8 +484,8 @@ module With_bounds = struct
       (allowed * 'r) t =
     let type_info = Type_info.create ~type_expr ~modality ~deep_only in
     match t with
-    | No_with_bounds -> With_bounds (type_info, [])
-    | With_bounds (ty, tys) -> With_bounds (type_info, ty :: tys)
+    | No_with_bounds -> With_bounds (type_info :: [])
+    | With_bounds (ty :: tys) -> With_bounds (type_info :: ty :: tys)
 
   (* CR aspsmith: This should be refactored to operate holistically (eg on Bounds.t)
      rather than per-axis. *)
@@ -514,10 +593,8 @@ module With_bounds = struct
         | Continue ctl_after_unpacking_b -> (
           match jkind_of_type b with
           | Some b_jkind ->
-            let b_bound = Bounds.get ~axis b_jkind.jkind.upper_bounds in
-            let types_on_axis =
-              With_bounds.types_on_axis ~axis b_jkind.jkind.with_bounds
-            in
+            let b_bound = Jkind_bounds.get ~axis b_jkind.jkind.upper_bounds in
+            let types_on_axis = types_on_axis ~axis b_jkind.jkind.with_bounds in
             let bound_so_far = A.join bound_so_far b_bound in
             let bound_so_far =
               loop ctl_after_unpacking_b bound_so_far types_on_axis
@@ -536,7 +613,33 @@ module With_bounds = struct
 end
 
 module Bounds = struct
-  include Jkind_types.Bounds
+  include Types.Jkind_bounds
+
+  let equal bounds1 bounds2 =
+    Fold2.f
+      { f =
+          (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 ->
+            let (module Bound_ops) = Axis.get axis in
+            Bound_ops.equal bound1 bound2)
+      }
+      ~combine:( && ) bounds1 bounds2
+
+  let debug_print ppf
+      { locality;
+        linearity;
+        uniqueness;
+        portability;
+        contention;
+        externality;
+        nullability
+      } =
+    Format.fprintf ppf
+      "@[{ locality = %a;@ linearity = %a;@ uniqueness = %a;@ portability = \
+       %a;@ contention = %a;@ externality = %a;@ nullability = %a }@]"
+      Mode.Locality.Const.print locality Mode.Linearity.Const.print linearity
+      Mode.Uniqueness.Const.print uniqueness Mode.Portability.Const.print
+      portability Mode.Contention.Const.print contention Externality.print
+      externality Nullability.print nullability
 
   let min =
     Create.f
@@ -582,6 +685,89 @@ module Bounds = struct
       }
 end
 
+module Layout_and_axes = struct
+  module Allow_disallow = Allowance.Magic_allow_disallow (struct
+    type (_, 'layout, 'd) sided = ('layout, 'd) layout_and_axes
+
+    let disallow_left t =
+      { t with with_bounds = With_bounds.disallow_left t.with_bounds }
+
+    let disallow_right t =
+      { t with with_bounds = With_bounds.disallow_right t.with_bounds }
+
+    let allow_left t =
+      { t with with_bounds = With_bounds.allow_left t.with_bounds }
+
+    let allow_right t =
+      { t with with_bounds = With_bounds.allow_right t.with_bounds }
+  end)
+
+  include Allow_disallow
+
+  let map f t = { t with layout = f t.layout }
+
+  let map_option f t =
+    match f t.layout with None -> None | Some layout -> Some { t with layout }
+
+  let map_type_expr f t =
+    { t with with_bounds = With_bounds.map_type_expr f t.with_bounds }
+
+  let equal eq_layout ({ layout = lay1; upper_bounds = bounds1; with_bounds = _ })
+        ({ layout = lay2; upper_bounds = bounds2; with_bounds = _ }) =
+    eq_layout lay1 lay2 && Bounds.equal bounds1 bounds2
+
+  let try_allow_l :
+      type l r.
+      ('layout, l * r) layout_and_axes ->
+      ('layout, Allowance.allowed * r) layout_and_axes option =
+   fun { layout; upper_bounds; with_bounds } ->
+    match With_bounds.try_allow_l with_bounds with
+    | None -> None
+    | Some with_bounds ->
+      Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds }
+
+  let try_allow_r { layout; upper_bounds; with_bounds } =
+    match With_bounds.try_allow_r with_bounds with
+    | Some with_bounds ->
+      Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds }
+    | None -> None
+
+  let debug_print ~print_type_expr format_layout ppf { layout; upper_bounds; with_bounds } =
+    Format.fprintf ppf "{ layout = %a;@ upper_bounds = %a;@ with_bounds = %a }"
+      format_layout layout Bounds.debug_print upper_bounds
+      (With_bounds.debug_print ~print_type_expr)
+      with_bounds
+end
+
+(*********************************)
+
+include Allowance.Magic_allow_disallow (struct
+  type (_, _, 'd) sided = 'd jkind
+
+  let disallow_right t =
+    { t with jkind = Layout_and_axes.disallow_right t.jkind }
+
+  let disallow_left t = { t with jkind = Layout_and_axes.disallow_left t.jkind }
+
+  let allow_right t = { t with jkind = Layout_and_axes.allow_right t.jkind }
+
+  let allow_left t = { t with jkind = Layout_and_axes.allow_left t.jkind }
+end)
+
+let try_allow_r t =
+  Option.map
+    (fun jkind -> { t with jkind })
+    (Layout_and_axes.try_allow_r t.jkind)
+
+let fresh_jkind jkind ~annotation ~why =
+  { jkind; annotation; history = Creation why; has_warned = false }
+  |> allow_left |> allow_right
+
+(* This version propagates the allowances from the [jkind] to the output. *)
+let fresh_jkind_poly jkind ~annotation ~why =
+  { jkind; annotation; history = Creation why; has_warned = false }
+
+
 (***********************)
 (*** constant jkinds ***)
 
@@ -610,29 +796,30 @@ let outcometree_of_modalities_new = ref (fun _ _ _ -> assert false)
 let set_outcometree_of_modalities_new p = outcometree_of_modalities_new := p
 
 module Const = struct
-  open Jkind_types.Layout_and_axes
-
-  type 'd t = (type_expr, 'd) Jkind_types.Const.t
+  type 'd t = (Layout.Const.t, 'd) Types.layout_and_axes
 
   include Layout_and_axes.Allow_disallow
 
   let max =
-    { layout = Layout.Const.max;
-      upper_bounds = Bounds.max;
-      with_bounds = No_with_bounds
-    }
+    Types.
+      { layout = Layout.Const.max;
+        upper_bounds = Bounds.max;
+        with_bounds = No_with_bounds
+      }
 
   let no_with_bounds_and_equal t1 t2 =
     let open Misc.Stdlib.Monad.Option.Syntax in
     let t1_t2 =
-      let* t1 = try_allow_l t1 in
-      let* t1 = try_allow_r t1 in
-      let* t2 = try_allow_l t2 in
-      let* t2 = try_allow_r t2 in
+      let* t1 = Layout_and_axes.try_allow_l t1 in
+      let* t1 = Layout_and_axes.try_allow_r t1 in
+      let* t2 = Layout_and_axes.try_allow_l t2 in
+      let* t2 = Layout_and_axes.try_allow_r t2 in
       Some (t1, t2)
     in
     match t1_t2 with
-    | Some (t1, t2) -> equal Layout.Const.equal t1 t2
+    | Some (t1, t2) ->
+      Layout.Const.equal t1.layout t2.layout
+        && Bounds.equal t1.upper_bounds t2.upper_bounds
     | None -> false
 
   module Builtin = struct
@@ -857,7 +1044,7 @@ module Const = struct
            (Some [])
 
     (** Write [actual] in terms of [base] *)
-    let convert_with_base ~(base : Builtin.t) actual =
+    let convert_with_base ~(base : Builtin.t) (actual : _ t) =
       let matching_layouts =
         Layout.Const.equal base.jkind.layout actual.layout
       in
@@ -866,10 +1053,10 @@ module Const = struct
       in
       let printable_with_bounds =
         List.map
-          (fun With_bounds.Type_info.{ type_expr; modality; _ } ->
+          (fun Types.{ type_expr; modality; _ } ->
             ( !outcometree_of_type_scheme type_expr,
               !outcometree_of_modalities_new Types.Immutable [] modality ))
-          (With_bounds.as_list actual.with_bounds)
+          (With_bounds.to_list actual.with_bounds)
       in
       match matching_layouts, modal_bounds with
       | true, Some modal_bounds ->
@@ -977,7 +1164,7 @@ module Const = struct
     in
     let layouts, upper_bounds, with_bounds =
       List.fold_left folder
-        ([], Bounds.min, Jkind_types.With_bounds.No_with_bounds)
+        ([], Bounds.min, No_with_bounds)
         jkinds
     in
     { layout = Layout.Const.Product (List.rev layouts);
@@ -1084,7 +1271,7 @@ module Const = struct
 end
 
 module Desc = struct
-  type 'd t = (type_expr, Sort.Flat.t Layout.t, 'd) Layout_and_axes.t
+  type 'd t = (Sort.Flat.t Layout.t, 'd) layout_and_axes
 
   let get_const t = Layout_and_axes.map_option Layout.get_flat_const t
 
@@ -1111,10 +1298,6 @@ module Desc = struct
 end
 
 module Jkind_desc = struct
-  open Jkind_types.Layout_and_axes
-
-  type nonrec 'd t = (Types.type_expr, Sort.t Layout.t, 'd) t
-
   let of_const t = Layout_and_axes.map Layout.of_const t
 
   let add_nullability_crossing t =
@@ -1176,9 +1359,9 @@ module Jkind_desc = struct
 
   let sub (type l r) ~type_equal ~jkind_of_type
       ({ layout = lay1; upper_bounds = bounds1; with_bounds = with_bounds1 } :
-        (allowed * r) t)
+        (allowed * r) jkind_desc)
       ({ layout = lay2; upper_bounds = bounds2; with_bounds = with_bounds2 } :
-        (l * allowed) t) =
+        (l * allowed) jkind_desc) =
     let bounds =
       (* CR aspsmith: iterating axis-first here (specifically for With_bounds.reduce)
          rather than type-first is probably the wrong choice; this is an artifact of when
@@ -1194,7 +1377,7 @@ module Jkind_desc = struct
              | No_with_bounds, No_with_bounds ->
                Axis_ops.less_or_equal bound1 bound2
              (* CR layouts v2.8: This should expand types on the left. *)
-             | (With_bounds (_, _) as wbs), No_with_bounds ->
+             | (With_bounds _ as wbs), No_with_bounds ->
                if Axis_ops.le Axis_ops.max bound2
                then Less
                else
@@ -1259,7 +1442,7 @@ module Jkind_desc = struct
         List.fold_right
           (fun (type_expr, modality) bounds ->
             With_bounds.add ~deep_only:false ~type_expr ~modality bounds)
-          tys_modalities Jkind_types.With_bounds.No_with_bounds
+          tys_modalities No_with_bounds
       in
       { layout; upper_bounds; with_bounds }
 
@@ -1345,7 +1528,7 @@ module Builtin = struct
       Layout.product
         (List.init arity (fun _ -> fst (Layout.of_new_sort_var ())))
     in
-    let desc : _ Jkind_desc.t =
+    let desc : _ jkind_desc =
       { layout; upper_bounds = Bounds.max; with_bounds = No_with_bounds }
     in
     fresh_jkind_poly desc ~annotation:None ~why:(Product_creation why)
@@ -1360,7 +1543,7 @@ let add_with_bounds ~modality ~type_expr t =
       Jkind_desc.add_with_bounds ~deep_only:true ~type_expr ~modality t.jkind
   }
 
-let has_with_bounds (type l r) (t : (l * r) t) =
+let has_with_bounds (type l r) (t : (l * r) jkind) =
   match t.jkind.with_bounds with
   | No_with_bounds -> false
   | With_bounds _ -> true
@@ -2008,8 +2191,8 @@ module Violation = struct
   open Format
 
   type violation =
-    | Not_a_subjkind : (allowed * 'r1) t * ('l * 'r2) t -> violation
-    | No_intersection : 'd t * ('l * allowed) t -> violation
+    | Not_a_subjkind : (allowed * 'r1) jkind * ('l * 'r2) jkind -> violation
+    | No_intersection : 'd jkind * ('l * allowed) jkind -> violation
 
   type nonrec t =
     { violation : violation;
@@ -2058,7 +2241,7 @@ module Violation = struct
       else
         dprintf "%s a sub%s of %a" verb layout_or_kind format_layout_or_kind k2
     in
-    let Pack k1, Pack k2, fmt_k1, fmt_k2, missing_cmi_option =
+    let Pack_jkind k1, Pack_jkind k2, fmt_k1, fmt_k2, missing_cmi_option =
       match t with
       | { violation = Not_a_subjkind (k1, k2); missing_cmi } -> (
         let missing_cmi =
@@ -2072,21 +2255,21 @@ module Violation = struct
         in
         match missing_cmi with
         | None ->
-          ( Pack k1,
-            Pack k2,
+          ( Pack_jkind k1,
+            Pack_jkind k2,
             dprintf "%s %a" layout_or_kind format_layout_or_kind k1,
             subjkind_format "is not" k2,
             None )
         | Some p ->
-          ( Pack k1,
-            Pack k2,
+          ( Pack_jkind k1,
+            Pack_jkind k2,
             dprintf "an unknown %s" layout_or_kind,
             subjkind_format "might not be" k2,
             Some p ))
       | { violation = No_intersection (k1, k2); missing_cmi } ->
         assert (Option.is_none missing_cmi);
-        ( Pack k1,
-          Pack k2,
+        ( Pack_jkind k1,
+          Pack_jkind k2,
           dprintf "%s %a" layout_or_kind format_layout_or_kind k1,
           dprintf "does not overlap with %a" format_layout_or_kind k2,
           None )
@@ -2154,7 +2337,7 @@ let score_reason = function
   | Creation (Concrete_creation _ | Concrete_legacy_creation _) -> -1
   | _ -> 0
 
-let combine_histories ~type_equal ~jkind_of_type reason (Pack k1) (Pack k2) =
+let combine_histories ~type_equal ~jkind_of_type reason (Pack_jkind k1) (Pack_jkind k2) =
   if flattened_histories
   then
     let choose_higher_scored_history history_a history_b =
@@ -2182,9 +2365,9 @@ let combine_histories ~type_equal ~jkind_of_type reason (Pack k1) (Pack k2) =
   else
     Interact
       { reason;
-        jkind1 = Pack k1.jkind;
+        jkind1 = Pack_jkind_desc k1.jkind;
         history1 = k1.history;
-        jkind2 = Pack k2.jkind;
+        jkind2 = Pack_jkind_desc k2.jkind;
         history2 = k2.history
       }
 
@@ -2200,13 +2383,13 @@ let intersection_or_error ~type_equal ~jkind_of_type ~reason t1 t2 =
       { jkind;
         annotation = None;
         history =
-          combine_histories ~type_equal ~jkind_of_type reason (Pack t1)
-            (Pack t2);
+          combine_histories ~type_equal ~jkind_of_type reason (Pack_jkind t1)
+            (Pack_jkind t2);
         has_warned = t1.has_warned || t2.has_warned
       }
 
-let round_up (type l r) ~type_equal ~jkind_of_type (t : (allowed * r) t) :
-    (l * allowed) t =
+let round_up (type l r) ~type_equal ~jkind_of_type (t : (allowed * r) jkind) :
+    (l * allowed) jkind =
   let upper_bounds =
     Bounds.Create.f
       { f =
@@ -2248,8 +2431,8 @@ let sub_jkind_l ~type_equal ~jkind_of_type sub super =
     Ok
       { sub with
         history =
-          combine_histories ~type_equal ~jkind_of_type Subjkind (Pack sub)
-            (Pack super)
+          combine_histories ~type_equal ~jkind_of_type Subjkind (Pack_jkind sub)
+            (Pack_jkind super)
       }
   in
   let failure = Error (Violation.of_ (Not_a_subjkind (sub, super))) in
@@ -2498,9 +2681,9 @@ module Debug_printers = struct
     function
     | Interact
         { reason;
-          jkind1 = Pack jkind1;
+          jkind1 = Pack_jkind_desc jkind1;
           history1;
-          jkind2 = Pack jkind2;
+          jkind2 = Pack_jkind_desc jkind2;
           history2
         } ->
       fprintf ppf
@@ -2511,7 +2694,7 @@ module Debug_printers = struct
     | Creation c -> fprintf ppf "Creation (%a)" creation_reason c
 
   let t ~print_type_expr ppf
-      ({ jkind; annotation = a; history = h; has_warned = _ } : 'd t) : unit =
+      ({ jkind; annotation = a; history = h; has_warned = _ } : 'd jkind) : unit =
     fprintf ppf "@[<v 2>{ jkind = %a@,; annotation = %a@,; history = %a }@]"
       (Jkind_desc.Debug_printers.t ~print_type_expr)
       jkind
@@ -2519,6 +2702,7 @@ module Debug_printers = struct
       a (history ~print_type_expr) h
 
   module Const = struct
+
     let t ~print_type_expr ppf
         ({ layout; upper_bounds; with_bounds } : _ Const.t) =
       fprintf ppf
diff --git a/typing/jkind.mli b/typing/jkind.mli
index 99f6186613c..13995f3e45f 100644
--- a/typing/jkind.mli
+++ b/typing/jkind.mli
@@ -117,20 +117,11 @@ end
     the meets (intersections) of r-jkinds and check that an l-jkind is less
     than an r-jkind.
 *)
-type 'd t = (Types.type_expr, 'd) Jkind_types.t
 
-type jkind_l := Types.jkind_l
-
-type jkind_r := Types.jkind_r
-
-type jkind_lr := Types.jkind_lr
-
-type packed = Pack : 'd t -> packed [@@unboxed]
-
-include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd t
+include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd Types.jkind
 
 (** Try to treat this jkind as an r-jkind. *)
-val try_allow_r : ('l * 'r) t -> ('l * allowed) t option
+val try_allow_r : ('l * 'r) Types.jkind -> ('l * allowed) Types.jkind option
 
 module History : sig
   include module type of struct
@@ -139,15 +130,15 @@ module History : sig
 
   (* history *)
 
-  val is_imported : 'd t -> bool
+  val is_imported : 'd Types.jkind -> bool
 
-  val update_reason : 'd t -> creation_reason -> 'd t
+  val update_reason : 'd Types.jkind -> creation_reason -> 'd Types.jkind
 
   (* Mark the jkind as having produced a compiler warning. *)
-  val with_warning : 'd t -> 'd t
+  val with_warning : 'd Types.jkind -> 'd Types.jkind
 
   (* Whether this jkind has produced a compiler warning. *)
-  val has_warned : 'd t -> bool
+  val has_warned : 'd Types.jkind -> bool
 end
 
 (******************************)
@@ -158,8 +149,8 @@ module Violation : sig
     (* [Not_a_subjkind] allows l-jkinds on the right so that it can be used
        in [sub_jkind_l]. There is no downside to this, as the printing
        machinery works over l-jkinds. *)
-    | Not_a_subjkind : (allowed * 'r1) t * ('l * 'r2) t -> violation
-    | No_intersection : 'd t * ('l * allowed) t -> violation
+    | Not_a_subjkind : (allowed * 'r1) Types.jkind * ('l * 'r2) Types.jkind -> violation
+    | No_intersection : 'd Types.jkind * ('l * allowed) Types.jkind -> violation
 
   type t
 
@@ -285,24 +276,24 @@ module Builtin : sig
   (** This jkind is the top of the jkind lattice. All types have jkind [any].
     But we cannot compile run-time manipulations of values of types with jkind
     [any]. *)
-  val any : why:History.any_creation_reason -> 'd t
+  val any : why:History.any_creation_reason -> 'd Types.jkind
 
   (** Value of types of this jkind are not retained at all at runtime *)
-  val void : why:History.void_creation_reason -> 'd t
+  val void : why:History.void_creation_reason -> 'd Types.jkind
 
-  val value_or_null : why:History.value_or_null_creation_reason -> 'd t
+  val value_or_null : why:History.value_or_null_creation_reason -> 'd Types.jkind
 
   (** This is the jkind of normal ocaml values *)
-  val value : why:History.value_creation_reason -> 'd t
+  val value : why:History.value_creation_reason -> 'd Types.jkind
 
   (** This is suitable for records or variants without mutable fields. *)
-  val immutable_data : why:History.value_creation_reason -> 'd t
+  val immutable_data : why:History.value_creation_reason -> 'd Types.jkind
 
   (** This is suitable for records or variants with mutable fields. *)
-  val mutable_data : why:History.value_creation_reason -> 'd t
+  val mutable_data : why:History.value_creation_reason -> 'd Types.jkind
 
   (** We know for sure that values of types of this jkind are always immediate *)
-  val immediate : why:History.immediate_creation_reason -> 'd t
+  val immediate : why:History.immediate_creation_reason -> 'd Types.jkind
 
   (** Build a jkind of unboxed products, from a list of types with
       their layouts. Errors if zero inputs are given. If only one input
@@ -313,76 +304,76 @@ module Builtin : sig
       This returns an [jkind_l] simply as a matter of convenience; it can be
       generalized if need be.  *)
   val product :
-    jkind_of_first_type:(unit -> jkind_l) ->
+    jkind_of_first_type:(unit -> Types.jkind_l) ->
     why:History.product_creation_reason ->
     (Types.type_expr * Mode.Modality.Value.Const.t) list ->
     Sort.t Layout.t list ->
-    jkind_l
+    Types.jkind_l
 
   (** Build a jkind of unboxed products, given only an arity. This jkind
       will not mode-cross, even though unboxed products generally should.
       This is useful when creating an initial jkind in Typedecl. *)
-  val product_of_sorts : why:History.product_creation_reason -> int -> jkind_l
+  val product_of_sorts : why:History.product_creation_reason -> int -> Types.jkind_l
 end
 
 (** Take an existing [t] and add an ability to cross across the nullability axis. *)
-val add_nullability_crossing : 'd t -> 'd t
+val add_nullability_crossing : 'd Types.jkind -> 'd Types.jkind
 
 (** Take an existing [jkind_l] and add some with-bounds. *)
 val add_with_bounds :
   modality:Mode.Modality.Value.Const.t ->
   type_expr:Types.type_expr ->
-  jkind_l ->
-  jkind_l
+  Types.jkind_l ->
+  Types.jkind_l
 
 (** Does this jkind have with-bounds? *)
-val has_with_bounds : jkind_l -> bool
+val has_with_bounds : Types.jkind_l -> bool
 
 (** Take an existing [t] and add an ability to mode-cross along the portability and
     contention axes, if [from] crosses the respective axes. Return the new jkind,
     along with a boolean of whether illegal crossing was added *)
 val add_portability_and_contention_crossing :
-  from:'d t -> (allowed * 'r) t -> (allowed * 'r) t * bool
+  from:'d Types.jkind -> (allowed * 'r) Types.jkind -> (allowed * 'r) Types.jkind * bool
 
 (******************************)
 (* construction *)
 
 (** Create a fresh sort variable, packed into a jkind, returning both
     the resulting kind and the sort. *)
-val of_new_sort_var : why:History.concrete_creation_reason -> 'd t * sort
+val of_new_sort_var : why:History.concrete_creation_reason -> 'd Types.jkind * sort
 
 (** Create a fresh sort variable, packed into a jkind. *)
-val of_new_sort : why:History.concrete_creation_reason -> 'd t
+val of_new_sort : why:History.concrete_creation_reason -> 'd Types.jkind
 
 (** Same as [of_new_sort_var], but the jkind is lowered to [Non_null]
     to mirror "legacy" OCaml values.
     Defaulting the sort variable produces exactly [value].  *)
 val of_new_legacy_sort_var :
-  why:History.concrete_legacy_creation_reason -> 'd t * sort
+  why:History.concrete_legacy_creation_reason -> 'd Types.jkind * sort
 
 (** Same as [of_new_sort], but the jkind is lowered to [Non_null]
     to mirror "legacy" OCaml values.
     Defaulting the sort variable produces exactly [value].  *)
-val of_new_legacy_sort : why:History.concrete_legacy_creation_reason -> 'd t
+val of_new_legacy_sort : why:History.concrete_legacy_creation_reason -> 'd Types.jkind
 
 val of_const :
   annotation:Parsetree.jkind_annotation option ->
   why:History.creation_reason ->
   'd Const.t ->
-  'd t
+  'd Types.jkind
 
-val of_builtin : why:History.creation_reason -> Const.Builtin.t -> 'd t
+val of_builtin : why:History.creation_reason -> Const.Builtin.t -> 'd Types.jkind
 
 val of_annotation :
   context:('l * allowed) History.annotation_context ->
   Parsetree.jkind_annotation ->
-  ('l * allowed) t
+  ('l * allowed) Types.jkind
 
 val of_annotation_option_default :
-  default:('l * allowed) t ->
+  default:('l * allowed) Types.jkind ->
   context:('l * allowed) History.annotation_context ->
   Parsetree.jkind_annotation option ->
-  ('l * allowed) t
+  ('l * allowed) Types.jkind
 
 (** Find a jkind from a type declaration. Type declarations are special because
     the jkind may have been provided via [: jkind] syntax (which goes through
@@ -398,7 +389,7 @@ val of_type_decl :
   context:History.annotation_context_l ->
   transl_type:(Parsetree.core_type -> Types.type_expr) ->
   Parsetree.type_declaration ->
-  (jkind_l * Parsetree.jkind_annotation option) option
+  (Types.jkind_l * Parsetree.jkind_annotation option) option
 
 (** Find a jkind from a type declaration in the same way as [of_type_decl],
     defaulting to ~default.
@@ -408,29 +399,29 @@ val of_type_decl :
 val of_type_decl_default :
   context:History.annotation_context_l ->
   transl_type:(Parsetree.core_type -> Types.type_expr) ->
-  default:jkind_l ->
+  default:Types.jkind_l ->
   Parsetree.type_declaration ->
-  jkind_l
+  Types.jkind_l
 
 (** Choose an appropriate jkind for a boxed record type *)
-val for_boxed_record : Types.label_declaration list -> jkind_l
+val for_boxed_record : Types.label_declaration list -> Types.jkind_l
 
 (** Choose an appropriate jkind for an unboxed record type. Uses
     [jkind_of_first_type] only in the singleton case, where the jkind of the
     unboxed record must match that of the single field. *)
 val for_unboxed_record :
-  jkind_of_first_type:(unit -> jkind_l) ->
+  jkind_of_first_type:(unit -> Types.jkind_l) ->
   Types.label_declaration list ->
-  jkind_l
+  Types.jkind_l
 
 (** Choose an appropriate jkind for a boxed variant type. *)
-val for_boxed_variant : Types.constructor_declaration list -> jkind_l
+val for_boxed_variant : Types.constructor_declaration list -> Types.jkind_l
 
 (** The jkind of an arrow type. *)
-val for_arrow : jkind_l
+val for_arrow : Types.jkind_l
 
 (** The jkind of an object type.  *)
-val for_object : jkind_l
+val for_object : Types.jkind_l
 
 (******************************)
 (* elimination and defaulting *)
@@ -439,8 +430,7 @@ module Desc : sig
   (** The description of a jkind, used as a return type from [get].  This
       description has no sort variables, but it might have [with]-types and thus
       needs the allowance machinery. *)
-  type 'd t =
-    (Types.type_expr, Sort.Flat.t Layout.t, 'd) Jkind_types.Layout_and_axes.t
+  type 'd t = (Sort.Flat.t Layout.t, 'd) Types.layout_and_axes
 
   val get_const : 'd t -> 'd Const.t option
 
@@ -448,59 +438,59 @@ module Desc : sig
 end
 
 (** Get a description of a jkind. *)
-val get : 'd t -> 'd Desc.t
+val get : 'd Types.jkind -> 'd Desc.t
 
 (** [get_layout_defaulting_to_value] extracts a constant layout, defaulting
     any sort variable to [value]. *)
-val get_layout_defaulting_to_value : 'd t -> Layout.Const.t
+val get_layout_defaulting_to_value : 'd Types.jkind -> Layout.Const.t
 
 (** [get_const] returns a [Const.t] if the layout has no sort variables,
     returning [None] otherwise *)
-val get_const : 'd t -> 'd Const.t option
+val get_const : 'd Types.jkind -> 'd Const.t option
 
 (** [default_to_value t] is [ignore (get_layout_defaulting_to_value t)] *)
-val default_to_value : 'd t -> unit
+val default_to_value : 'd Types.jkind -> unit
 
 (** [is_void t] is [Void = get_layout_defaulting_to_value t].  In particular, it
     will default the jkind to value if needed to make this false. *)
-val is_void_defaulting : 'd t -> bool
+val is_void_defaulting : 'd Types.jkind -> bool
 (* CR layouts v5: When we have proper support for void, we'll want to change
    these three functions to default to void - it's the most efficient thing
    when we have a choice. *)
 
 (** Returns the sort corresponding to the jkind.  Call only on representable
     jkinds - raises on Any. *)
-val sort_of_jkind : jkind_l -> sort
+val sort_of_jkind : Types.jkind_l -> sort
 
 (** Gets the layout of a jkind; returns [None] if the layout is still unknown.
     Never does mutation. *)
-val get_layout : 'd t -> Layout.Const.t option
+val get_layout : 'd Types.jkind -> Layout.Const.t option
 
 (* CR reisenberg: do we need [extract_layout]? *)
 
 (** Gets the layout of a jkind, without looking through sort variables. *)
-val extract_layout : 'd t -> Sort.t Layout.t
+val extract_layout : 'd Types.jkind -> Sort.t Layout.t
 
 (** Gets the maximum modes for types of this jkind. *)
 val get_modal_upper_bounds :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  'd t ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  'd Types.jkind ->
   Mode.Alloc.Const.t
 
 (** Gets the maximum mode on the externality axis for types of this jkind. *)
 val get_externality_upper_bound :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  'd t ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  'd Types.jkind ->
   Externality.t
 
 (** Computes a jkind that is the same as the input but with an updated maximum
     mode for the externality axis *)
-val set_externality_upper_bound : jkind_r -> Externality.t -> jkind_r
+val set_externality_upper_bound : Types.jkind_r -> Externality.t -> Types.jkind_r
 
 (** Sets the layout in a jkind. *)
-val set_layout : 'd t -> Sort.t Layout.t -> 'd t
+val set_layout : 'd Types.jkind -> Sort.t Layout.t -> 'd Types.jkind
 
 (** Extract out component jkinds from the product. Because there are no product
     jkinds, this is a bit of a lie: instead, this decomposes the layout but just
@@ -508,10 +498,10 @@ val set_layout : 'd t -> Sort.t Layout.t -> 'd t
     Because it just reuses the mode information, the resulting jkinds are higher
     in the jkind lattice than they might need to be.
     *)
-val decompose_product : 'd t -> 'd t list option
+val decompose_product : 'd Types.jkind -> 'd Types.jkind list option
 
 (** Get an annotation (that a user might write) for this [t]. *)
-val get_annotation : 'd t -> Parsetree.jkind_annotation option
+val get_annotation : 'd Types.jkind -> Parsetree.jkind_annotation option
 
 (*********************************)
 (* pretty printing *)
@@ -527,7 +517,7 @@ val set_outcometree_of_modalities_new :
   Outcometree.out_mode_new list) ->
   unit
 
-val format : Format.formatter -> 'd t -> unit
+val format : Format.formatter -> 'd Types.jkind -> unit
 
 (** Format the history of this jkind: what interactions it has had and why
     it is the jkind that it is. Might be a no-op: see [display_histories]
@@ -535,7 +525,7 @@ val format : Format.formatter -> 'd t -> unit
 
     The [intro] is something like "The jkind of t is". *)
 val format_history :
-  intro:(Format.formatter -> unit) -> Format.formatter -> 'd t -> unit
+  intro:(Format.formatter -> unit) -> Format.formatter -> 'd Types.jkind -> unit
 
 (** Provides the [Printtyp.path] formatter back up the dependency chain to
     this module. *)
@@ -547,20 +537,20 @@ val set_printtyp_path : (Format.formatter -> Path.t -> unit) -> unit
 (** This checks for equality, and sets any variables to make two jkinds
     equal, if possible. e.g. [equate] on a var and [value] will set the
     variable to be [value] *)
-val equate : jkind_lr -> jkind_lr -> bool
+val equate : Types.jkind_lr -> Types.jkind_lr -> bool
 
 (** This checks for equality, but has the invariant that it can only be called
     when there is no need for unification; e.g. [equal] on a var and [value]
     will crash.
 
     CR layouts (v1.5): At the moment, this is actually the same as [equate]! *)
-val equal : jkind_lr -> jkind_lr -> bool
+val equal : Types.jkind_lr -> Types.jkind_lr -> bool
 
 (** Checks whether two jkinds have a non-empty intersection. Might mutate
     sort variables. Works over any mix of l- and r-jkinds, because the only
     way not to have an intersection is by looking at the layout: all axes
     have a bottom element. *)
-val has_intersection : 'd1 t -> 'd2 t -> bool
+val has_intersection : 'd1 Types.jkind -> 'd2 Types.jkind -> bool
 
 (** Finds the intersection of two jkinds, constraining sort variables to
     create one if needed, or returns a [Violation.t] if an intersection does
@@ -571,19 +561,19 @@ val has_intersection : 'd1 t -> 'd2 t -> bool
     intersection of the two, not something that modifies the second jkind. *)
 val intersection_or_error :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
   reason:History.interact_reason ->
-  ('l1 * allowed) t ->
-  ('l2 * allowed) t ->
-  (('l1 * allowed) t, Violation.t) Result.t
+  ('l1 * allowed) Types.jkind ->
+  ('l2 * allowed) Types.jkind ->
+  (('l1 * allowed) Types.jkind, Violation.t) Result.t
 
 (** [sub t1 t2] says whether [t1] is a subjkind of [t2]. Might update
     either [t1] or [t2] to make their layouts equal.*)
 val sub :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  jkind_l ->
-  jkind_r ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  Types.jkind_l ->
+  Types.jkind_r ->
   bool
 
 type sub_or_intersect =
@@ -595,18 +585,18 @@ type sub_or_intersect =
     see comments there for more info. *)
 val sub_or_intersect :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  (allowed * 'r) t ->
-  ('l * allowed) t ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  (allowed * 'r) Types.jkind ->
+  ('l * allowed) Types.jkind ->
   sub_or_intersect
 
 (** [sub_or_error t1 t2] does a subtype check, returning an appropriate
     [Violation.t] upon failure. *)
 val sub_or_error :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  (allowed * 'r) t ->
-  ('l * allowed) t ->
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  (allowed * 'r) Types.jkind ->
+  ('l * allowed) Types.jkind ->
   (unit, Violation.t) result
 
 (** Like [sub], but returns the subjkind with an updated history.
@@ -619,34 +609,34 @@ val sub_or_error :
 *)
 val sub_jkind_l :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  jkind_l ->
-  jkind_l ->
-  (jkind_l, Violation.t) result
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  Types.jkind_l ->
+  Types.jkind_l ->
+  (Types.jkind_l, Violation.t) result
 
 (** "round up" a [jkind_l] to a [jkind_r] such that the input is less than the
     output. *)
 val round_up :
   type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
-  jkind_of_type:(Types.type_expr -> jkind_l option) ->
-  (allowed * 'r) t ->
-  ('l * allowed) t
+  jkind_of_type:(Types.type_expr -> Types.jkind_l option) ->
+  (allowed * 'r) Types.jkind ->
+  ('l * allowed) Types.jkind
 
 (** Map a function over types in [upper_bounds] *)
 val map_type_expr :
-  (Types.type_expr -> Types.type_expr) -> (allowed * 'r) t -> (allowed * 'r) t
+  (Types.type_expr -> Types.type_expr) -> (allowed * 'r) Types.jkind -> (allowed * 'r) Types.jkind
 
 (** Checks to see whether a jkind is the maximum jkind. Never does any
     mutation. *)
-val is_max : ('l * allowed) t -> bool
+val is_max : ('l * allowed) Types.jkind -> bool
 
 (** Checks to see whether a jkind has layout any. Never does any mutation. *)
-val has_layout_any : ('l * allowed) t -> bool
+val has_layout_any : ('l * allowed) Types.jkind -> bool
 
 (** Checks whether a jkind is [value]. This really should require a [jkind_lr],
     but it works on any [jkind], because it's used in printing and is somewhat
     unprincipled. *)
-val is_value_for_printing : 'd t -> bool
+val is_value_for_printing : 'd Types.jkind -> bool
 
 (*********************************)
 (* debugging *)
@@ -655,7 +645,7 @@ module Debug_printers : sig
   val t :
     print_type_expr:(Format.formatter -> Types.type_expr -> unit) ->
     Format.formatter ->
-    'd t ->
+    'd Types.jkind ->
     unit
 
   module Const : sig
diff --git a/typing/jkind_types.ml b/typing/jkind_types.ml
index 1a1f530371d..951158e4cb8 100644
--- a/typing/jkind_types.ml
+++ b/typing/jkind_types.ml
@@ -521,262 +521,3 @@ module Layout = struct
       | Product of t list
   end
 end
-
-module With_bounds = struct
-  module Type_info = struct
-    type +'type_expr t =
-      { type_expr : 'type_expr;
-        modality : Mode.Modality.Value.Const.t;
-        nullability : bool
-      }
-
-    let print ~print_type_expr ppf { type_expr; modality } =
-      let open Format in
-      if Mode.Modality.Value.Const.is_id modality
-      then print_type_expr ppf type_expr
-      else
-        fprintf ppf "(@[%a@ @@@@ %a])" print_type_expr type_expr
-          Mode.Modality.Value.Const.print modality
-
-    let map_type_expr f ({ type_expr; _ } as t) =
-      { t with type_expr = f type_expr }
-
-    let is_on_axis (type a) ~(axis : a Jkind_axis.Axis.t) t =
-      match axis with
-      | Nonmodal Externality -> true (* All fields matter for externality *)
-      | Nonmodal Nullability -> t.nullability
-      | Modal axis ->
-        let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
-        not
-          (Mode.Modality.Value.Const.proj axis t.modality
-          |> Mode.Modality.is_constant)
-
-    let compose_modality t ~then_ =
-      let modality = Mode.Modality.Value.Const.compose t.modality ~then_ in
-      assert (not (Mode.Modality.Value.Const.is_id modality));
-      { t with modality }
-
-    let create ~type_expr ~modality ~deep_only =
-      { type_expr; modality; nullability = not deep_only }
-  end
-
-  type (+'type_expr, 'd) t =
-    | No_with_bounds : ('type_expr, 'l * 'r) t
-    (* There must always be at least one type. *)
-    | With_bounds :
-        'type_expr Type_info.t * 'type_expr Type_info.t list
-        -> ('type_expr, 'l * Allowance.disallowed) t
-
-  let as_list : type l r. (_, l * r) t -> _ = function
-    | No_with_bounds -> []
-    | With_bounds (ty, tys) -> ty :: tys
-
-  let has_with_bounds : type l r. (_, l * r) t -> _ = function
-    | No_with_bounds -> false
-    | With_bounds _ -> true
-
-  open Allowance
-
-  include Magic_allow_disallow (struct
-    type ('type_expr, _, 'd) sided = ('type_expr, 'd) t constraint 'd = 'l * 'r
-
-    let disallow_left :
-        type l r. ('type_expr, l * r) t -> ('type_expr, disallowed * r) t =
-      function
-      | No_with_bounds -> No_with_bounds
-      | With_bounds _ as b -> b
-
-    let disallow_right :
-        type l r. ('type_expr, l * r) t -> ('type_expr, l * disallowed) t =
-      function
-      | No_with_bounds -> No_with_bounds
-      | With_bounds _ as b -> b
-
-    let allow_left :
-        type l r. ('type_expr, allowed * r) t -> ('type_expr, l * r) t =
-      function
-      | No_with_bounds -> No_with_bounds
-      | With_bounds _ as b -> b
-
-    let allow_right :
-        type l r. ('type_expr, l * allowed) t -> ('type_expr, l * r) t =
-      function
-      | No_with_bounds -> No_with_bounds
-  end)
-
-  let try_allow_l :
-      type l r. ('type_expr, l * r) t -> ('type_expr, allowed * r) t option =
-    function
-    | No_with_bounds -> Some No_with_bounds
-    | With_bounds _ as b -> Some b
-
-  let try_allow_r :
-      type l r. ('type_expr, l * r) t -> ('type_expr, l * allowed) t option =
-    function
-    | No_with_bounds -> Some No_with_bounds
-    | With_bounds _ -> None
-
-  let map_type_expr (type l r) f :
-      ('type_expr, l * r) t -> ('type_expr, l * r) t = function
-    | No_with_bounds -> No_with_bounds
-    | With_bounds (ty, tys) ->
-      let f' = Type_info.map_type_expr f in
-      With_bounds (f' ty, List.map f' tys)
-
-  let types_on_axis (type l r a) ~(axis : a Jkind_axis.Axis.t) :
-      (_, l * r) t -> _ = function
-    | No_with_bounds -> []
-    | With_bounds (ti, tis) ->
-      List.filter_map
-        (fun (type_info : _ Type_info.t) ->
-          if Type_info.is_on_axis ~axis type_info
-          then Some type_info.type_expr
-          else None)
-        (ti :: tis)
-
-  let compose_modality (type l r) ~then_ : (_, l * r) t -> (_, l * r) t =
-    function
-    | No_with_bounds -> No_with_bounds
-    | With_bounds (t, ts) ->
-      With_bounds
-        ( Type_info.compose_modality ~then_ t,
-          List.map (Type_info.compose_modality ~then_) ts )
-
-  let debug_print (type l r) ~print_type_expr ppf : (_, l * r) t -> _ =
-    let open Format in
-    function
-    | No_with_bounds -> fprintf ppf "No_with_bounds"
-    | With_bounds (ty, tys) ->
-      fprintf ppf "With_bounds @[[%a]@]"
-        (pp_print_list
-           ~pp_sep:(fun ppf () -> fprintf ppf ";@ ")
-           (Type_info.print ~print_type_expr))
-        (ty :: tys)
-end
-
-module Bounds = struct
-  open Jkind_axis
-  include Axis_collection.Indexed (Misc.Stdlib.Monad.Identity)
-
-  let equal bounds1 bounds2 =
-    Fold2.f
-      { f =
-          (fun (type axis) ~(axis : axis Axis.t) bound1 bound2 ->
-            let (module Bound_ops) = Axis.get axis in
-            Bound_ops.equal bound1 bound2)
-      }
-      ~combine:( && ) bounds1 bounds2
-
-  let debug_print ppf
-      { locality;
-        linearity;
-        uniqueness;
-        portability;
-        contention;
-        externality;
-        nullability
-      } =
-    Format.fprintf ppf
-      "@[{ locality = %a;@ linearity = %a;@ uniqueness = %a;@ portability = \
-       %a;@ contention = %a;@ externality = %a;@ nullability = %a }@]"
-      Mode.Locality.Const.print locality Mode.Linearity.Const.print linearity
-      Mode.Uniqueness.Const.print uniqueness Mode.Portability.Const.print
-      portability Mode.Contention.Const.print contention Externality.print
-      externality Nullability.print nullability
-end
-
-module Layout_and_axes = struct
-  type ('type_expr, 'layout, 'd) t =
-    { layout : 'layout;
-      upper_bounds : Bounds.t;
-      with_bounds : ('type_expr, 'd) With_bounds.t
-    }
-    constraint 'd = 'l * 'r
-
-  module Allow_disallow = Allowance.Magic_allow_disallow (struct
-    type ('type_expr, 'layout, 'd) sided = ('type_expr, 'layout, 'd) t
-
-    let disallow_left t =
-      { t with with_bounds = With_bounds.disallow_left t.with_bounds }
-
-    let disallow_right t =
-      { t with with_bounds = With_bounds.disallow_right t.with_bounds }
-
-    let allow_left t =
-      { t with with_bounds = With_bounds.allow_left t.with_bounds }
-
-    let allow_right t =
-      { t with with_bounds = With_bounds.allow_right t.with_bounds }
-  end)
-
-  include Allow_disallow
-
-  let map f t = { t with layout = f t.layout }
-
-  let map_option f t =
-    match f t.layout with None -> None | Some layout -> Some { t with layout }
-
-  let map_type_expr f t =
-    { t with with_bounds = With_bounds.map_type_expr f t.with_bounds }
-
-  let equal eq_layout { layout = lay1; upper_bounds = bounds1 }
-      { layout = lay2; upper_bounds = bounds2 } =
-    eq_layout lay1 lay2 && Bounds.equal bounds1 bounds2
-
-  let try_allow_l :
-      type l r.
-      ('type_expr, 'layout, l * r) t ->
-      ('type_expr, 'layout, Allowance.allowed * r) t option =
-   fun { layout; upper_bounds; with_bounds } ->
-    match With_bounds.try_allow_l with_bounds with
-    | None -> None
-    | Some with_bounds ->
-      Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds }
-
-  let try_allow_r { layout; upper_bounds; with_bounds } =
-    match With_bounds.try_allow_r with_bounds with
-    | Some with_bounds ->
-      Some { layout; upper_bounds = Obj.magic upper_bounds; with_bounds }
-    | None -> None
-
-  let debug_print ~print_type_expr format_layout ppf
-      { layout; upper_bounds; with_bounds } =
-    Format.fprintf ppf "{ layout = %a;@ upper_bounds = %a;@ with_bounds = %a }"
-      format_layout layout Bounds.debug_print upper_bounds
-      (With_bounds.debug_print ~print_type_expr)
-      with_bounds
-end
-
-module Jkind_desc = struct
-  type ('type_expr, 'd) t = ('type_expr, Sort.t Layout.t, 'd) Layout_and_axes.t
-
-  type 'type_expr packed = Pack : ('type_expr, 'd) t -> 'type_expr packed
-  [@@unboxed]
-end
-
-(* A history of conditions placed on a jkind.
-
-   INVARIANT: at most one sort variable appears in this history.
-   This is a natural consequence of producing this history by comparing
-   jkinds.
-*)
-type 'type_expr history =
-  | Interact of
-      { reason : Jkind_intf.History.interact_reason;
-        jkind1 : 'type_expr Jkind_desc.packed;
-        history1 : 'type_expr history;
-        jkind2 : 'type_expr Jkind_desc.packed;
-        history2 : 'type_expr history
-      }
-  | Creation of Jkind_intf.History.creation_reason
-
-type ('type_expr, 'd) t =
-  { jkind : ('type_expr, 'd) Jkind_desc.t;
-    annotation : Parsetree.jkind_annotation option;
-    history : 'type_expr history;
-    has_warned : bool
-  }
-
-module Const = struct
-  type ('type_expr, 'd) t = ('type_expr, Layout.Const.t, 'd) Layout_and_axes.t
-end
diff --git a/typing/jkind_types.mli b/typing/jkind_types.mli
index 2a07b42bdc2..0103bd4c718 100644
--- a/typing/jkind_types.mli
+++ b/typing/jkind_types.mli
@@ -105,129 +105,3 @@ module Layout : sig
       | Product of t list
   end
 end
-
-module With_bounds : sig
-  module Type_info : sig
-    type +'type_expr t =
-      { type_expr : 'type_expr;
-        modality : Mode.Modality.Value.Const.t;
-        nullability : bool
-      }
-
-    val create :
-      type_expr:'type_expr ->
-      modality:Mode.Modality.Value.Const.t ->
-      deep_only:bool ->
-      'type_expr t
-  end
-
-  type (+'type_expr, 'd) t =
-    | No_with_bounds : ('type_expr, 'l * 'r) t
-    (* There must always be at least one type. *)
-    | With_bounds :
-        'type_expr Type_info.t * 'type_expr Type_info.t list
-        -> ('type_expr, 'l * Allowance.disallowed) t
-
-  include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) t
-
-  val as_list : ('type_expr, 'l * 'r) t -> 'type_expr Type_info.t list
-
-  val has_with_bounds : ('type_expr, 'l * 'r) t -> bool
-
-  val types_on_axis :
-    axis:'a Jkind_axis.Axis.t -> ('type_expr, 'l * 'r) t -> 'type_expr list
-
-  val compose_modality :
-    then_:Mode.Modality.t -> ('type_expr, 'l * 'r) t -> ('type_expr, 'l * 'r) t
-
-  val debug_print :
-    print_type_expr:(Format.formatter -> 'type_expr -> unit) ->
-    Format.formatter ->
-    ('type_expr, 'l * 'r) t ->
-    unit
-end
-
-module Bounds : sig
-  include module type of
-      Jkind_axis.Axis_collection.Indexed (Misc.Stdlib.Monad.Identity)
-
-  val debug_print : Format.formatter -> t -> unit
-end
-
-module Layout_and_axes : sig
-  open Allowance
-
-  type (+'type_expr, 'layout, 'd) t =
-    { layout : 'layout;
-      upper_bounds : Bounds.t;
-      with_bounds : ('type_expr, 'd) With_bounds.t
-    }
-    constraint 'd = 'l * 'r
-
-  module type Allow_disallow :=
-    Allow_disallow with type ('a, 'b, 'd) sided := ('a, 'b, 'd) t
-
-  module Allow_disallow : Allow_disallow
-
-  include Allow_disallow
-
-  val map : ('a -> 'b) -> ('type_expr, 'a, 'd) t -> ('type_expr, 'b, 'd) t
-
-  val map_option :
-    ('a -> 'b option) -> ('type_expr, 'a, 'd) t -> ('type_expr, 'b, 'd) t option
-
-  val map_type_expr :
-    ('type_expr -> 'type_expr) ->
-    ('type_expr, 'a, 'd) t ->
-    ('type_expr, 'a, 'd) t
-
-  val equal :
-    ('layout -> 'layout -> bool) ->
-    ('type_expr, 'layout, allowed * allowed) t ->
-    ('type_expr, 'layout, allowed * allowed) t ->
-    bool
-
-  val try_allow_l :
-    ('type_expr, 'layout, 'l * 'r) t ->
-    ('type_expr, 'layout, allowed * 'r) t option
-
-  val try_allow_r :
-    ('type_expr, 'layout, 'l * 'r) t ->
-    ('type_expr, 'layout, 'l * allowed) t option
-
-  val debug_print :
-    print_type_expr:(Format.formatter -> 'type_expr -> unit) ->
-    (Format.formatter -> 'layout -> unit) ->
-    Format.formatter ->
-    ('type_expr, 'layout, 'd) t ->
-    unit
-end
-
-module Jkind_desc : sig
-  type (+'type_expr, 'd) t = ('type_expr, Sort.t Layout.t, 'd) Layout_and_axes.t
-
-  type +'type_expr packed = Pack : ('type_expr, 'd) t -> 'type_expr packed
-  [@@unboxed]
-end
-
-type +'type_expr history =
-  | Interact of
-      { reason : Jkind_intf.History.interact_reason;
-        jkind1 : 'type_expr Jkind_desc.packed;
-        history1 : 'type_expr history;
-        jkind2 : 'type_expr Jkind_desc.packed;
-        history2 : 'type_expr history
-      }
-  | Creation of Jkind_intf.History.creation_reason
-
-type (+'type_expr, 'd) t =
-  { jkind : ('type_expr, 'd) Jkind_desc.t;
-    annotation : Parsetree.jkind_annotation option;
-    history : 'type_expr history;
-    has_warned : bool
-  }
-
-(** CR layouts v2.8: remove this when printing is improved *)
-module Const : sig
-  type (+'type_expr, 'd) t = ('type_expr, Layout.Const.t, 'd) Layout_and_axes.t
-end
diff --git a/typing/types.ml b/typing/types.ml
index d23dc030abf..e01377ce5dd 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -28,6 +28,9 @@ let is_mutable = function
 
 (* Type expressions for the core language *)
 
+module Jkind_bounds =
+  Jkind_axis.Axis_collection.Indexed (Misc.Stdlib.Monad.Identity)
+
 type transient_expr =
   { mutable desc: type_desc;
     mutable level: int;
@@ -99,10 +102,55 @@ and _ commutable_gen =
   | Cunknown : [> `none] commutable_gen
   | Cvar : {mutable commu: any commutable_gen} -> [> `var] commutable_gen
 
-and 'd jkind = (type_expr, 'd) Jkind_types.t
+(* jkinds *)
+
+and jkind_history =
+  | Interact of
+      { reason : Jkind_intf.History.interact_reason;
+        jkind1 : jkind_desc_packed;
+        history1 : jkind_history;
+        jkind2 : jkind_desc_packed;
+        history2 : jkind_history
+      }
+  | Creation of Jkind_intf.History.creation_reason
+
+and with_bounds_type =
+  { type_expr : type_expr;
+    modality : Mode.Modality.Value.Const.t;
+    nullability : bool
+  }
+
+and 'd with_bounds =
+  | No_with_bounds : ('l * 'r) with_bounds
+  (* There must always be at least one type. *)
+  | With_bounds :
+      with_bounds_type Misc.Nonempty_list.t
+      -> ('l * Allowance.disallowed) with_bounds
+
+and ('layout, 'd) layout_and_axes =
+  { layout : 'layout;
+    upper_bounds : Jkind_bounds.t;
+    with_bounds : 'd with_bounds
+  }
+  constraint 'd = 'l * 'r
+
+and 'd jkind_desc = (Jkind_types.Sort.t Jkind_types.Layout.t, 'd) layout_and_axes
+  constraint 'd = 'l * 'r
+
+and jkind_desc_packed = Pack_jkind_desc : ('l * 'r) jkind_desc -> jkind_desc_packed
+
+and 'd jkind =
+  { jkind : 'd jkind_desc;
+    annotation : Parsetree.jkind_annotation option;
+    history : jkind_history;
+    has_warned : bool
+  }
+  constraint 'd = 'l * 'r
+
 and jkind_l = (allowed * disallowed) jkind
 and jkind_r = (disallowed * allowed) jkind
 and jkind_lr = (allowed * allowed) jkind
+and jkind_packed = Pack_jkind : ('l * 'r) jkind -> jkind_packed
 
 module TransientTypeOps = struct
   type t = type_expr
diff --git a/typing/types.mli b/typing/types.mli
index 3eccf3ba219..c2fa4896aa4 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -67,6 +67,10 @@ val is_mutable : mutability -> bool
 
     Note on mutability: TBD.
  *)
+
+module Jkind_bounds :
+  module type of Jkind_axis.Axis_collection.Indexed (Misc.Stdlib.Monad.Identity)
+
 type type_expr
 type row_desc
 type row_field
@@ -229,12 +233,62 @@ and abbrev_memo =
     This is only allowed when the real type is known.
 *)
 
-(** Jkinds classify types. *)
-(* CR layouts v2.8: Say more here. *)
-and 'd jkind = (type_expr, 'd) Jkind_types.t
+
+(**** Jkinds ****)
+
+(** A history of conditions placed on a jkind.
+
+   INVARIANT: at most one sort variable appears in this history.
+   This is a natural consequence of producing this history by comparing
+   jkinds.
+*)
+and jkind_history =
+  | Interact of
+      { reason : Jkind_intf.History.interact_reason;
+        jkind1 : jkind_desc_packed;
+        history1 : jkind_history;
+        jkind2 : jkind_desc_packed;
+        history2 : jkind_history
+      }
+  | Creation of Jkind_intf.History.creation_reason
+
+and with_bounds_type =
+  { type_expr : type_expr;
+    modality : Mode.Modality.Value.Const.t;
+    nullability : bool
+  }
+
+and 'd with_bounds =
+  | No_with_bounds : ('l * 'r) with_bounds
+  (* There must always be at least one type. *)
+  | With_bounds :
+      with_bounds_type Misc.Nonempty_list.t
+      -> ('l * Allowance.disallowed) with_bounds
+
+and ('layout, 'd) layout_and_axes =
+  { layout : 'layout;
+    upper_bounds : Jkind_bounds.t;
+    with_bounds : 'd with_bounds
+  }
+  constraint 'd = 'l * 'r
+
+and 'd jkind_desc = (Jkind_types.Sort.t Jkind_types.Layout.t, 'd) layout_and_axes
+  constraint 'd = 'l * 'r
+
+and jkind_desc_packed = Pack_jkind_desc : ('l * 'r) jkind_desc -> jkind_desc_packed
+
+and 'd jkind =
+  { jkind : 'd jkind_desc;
+    annotation : Parsetree.jkind_annotation option;
+    history : jkind_history;
+    has_warned : bool
+  }
+  constraint 'd = 'l * 'r
+
 and jkind_l = (allowed * disallowed) jkind  (* the jkind of an actual type *)
 and jkind_r = (disallowed * allowed) jkind  (* the jkind expected of a type *)
 and jkind_lr = (allowed * allowed) jkind    (* the jkind of a variable *)
+and jkind_packed = Pack_jkind : ('l * 'r) jkind -> jkind_packed
 
 val is_commu_ok: commutable -> bool
 val commu_ok: commutable
diff --git a/utils/misc.ml b/utils/misc.ml
index 3754781f948..8de941fbc05 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -1723,3 +1723,21 @@ let remove_double_underscores s =
   in
   loop 0;
   Buffer.contents buf
+
+module Nonempty_list = struct
+  type nonrec 'a t = ( :: ) of 'a * 'a list
+
+  let to_list (x :: xs) : _ list = x :: xs
+
+  let of_list_opt : _ list -> _ t option = function
+    | [] -> None
+    | (x :: xs)-> Some (x :: xs)
+
+  let map f (x :: xs) = f x :: List.map f xs
+
+  let pp_print ?pp_sep f ppf t =
+    Format.pp_print_list ?pp_sep f ppf (to_list t)
+
+  let (@) (x :: xs) (y :: ys) =
+    x :: List.(x :: (xs @ (y :: ys)))
+end
diff --git a/utils/misc.mli b/utils/misc.mli
index 88c481060df..f4a7f4a146a 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -1075,3 +1075,21 @@ type filepath = string
 type alerts = string Stdlib.String.Map.t
 
 val remove_double_underscores : string -> string
+
+(** Non-empty lists *)
+module Nonempty_list : sig
+  type nonrec 'a t = ( :: ) of 'a * 'a list
+
+  val to_list : 'a t -> 'a list
+  val of_list_opt : 'a list -> 'a t option
+  val map : ('a -> 'b) -> 'a t -> 'b t
+
+  val pp_print :
+    ?pp_sep:(Format.formatter -> unit -> unit) ->
+    (Format.formatter -> 'a -> unit) ->
+    Format.formatter ->
+    'a t ->
+    unit
+
+  val (@) : 'a t -> 'a t -> 'a t
+end