diff --git a/dune b/dune
index b632ab6dc07..32d657d558b 100644
--- a/dune
+++ b/dune
@@ -89,7 +89,7 @@
 
    ;; TYPING
    ident path jkind primitive shape shape_reduce types btype oprint subst predef datarepr
-   cmi_format persistent_env env errortrace mode jkind_types jkind_intf
+   global_module cmi_format persistent_env env errortrace mode jkind_types jkind_intf
    typedtree printtyped ctype printtyp includeclass mtype envaux includecore
    tast_iterator tast_mapper signature_group cmt_format cms_format untypeast
    includemod includemod_errorprinter
diff --git a/typing/global_module.ml b/typing/global_module.ml
new file mode 100644
index 00000000000..adaa40f3faa
--- /dev/null
+++ b/typing/global_module.ml
@@ -0,0 +1,232 @@
+[@@@ocaml.warning "+a-40-41-42"]
+
+let pp_concat pp ppf list =
+  Format.pp_print_list ~pp_sep:Format.pp_print_cut pp ppf list
+
+module Name : sig
+  type t = private {
+    head : string;
+    args : (t * t) list;
+  }
+
+  val create : string -> (t * t) list -> t
+
+  val unsafe_create_unchecked : string -> (t * t) list -> t
+
+  include Identifiable.S with type t := t
+end = struct
+  type t = {
+    head : string;
+    args : (t * t) list;
+  }
+
+  include Identifiable.Make (struct
+    type nonrec t = t
+
+    let rec compare
+        ({ head = head1; args = args1 } as t1)
+        ({ head = head2; args = args2 } as t2) =
+      if t1 == t2 then 0
+      else
+        match String.compare head1 head2 with
+        | 0 -> List.compare compare_arg args1 args2
+        | c -> c
+    and compare_arg (name1, arg1) (name2, arg2) =
+      match compare name1 name2 with
+      | 0 -> compare arg1 arg2
+      | c -> c
+
+    let equal t1 t2 = compare t1 t2 = 0
+
+    let rec print ppf ({ head; args } : t) =
+      match args with
+      | [] ->
+          (* Preserve simple non-wrapping behaviour in atomic case *)
+          Format.fprintf ppf "%s" head
+      | _ ->
+          Format.fprintf ppf "@[<hov 1>%s%a@]"
+            head
+            (pp_concat print_arg_pair) args
+    and print_arg_pair ppf (name, arg) =
+      Format.fprintf ppf "[%a:%a]" print name print arg
+
+    let output = print |> Misc.output_of_print
+
+    let hash = Hashtbl.hash
+  end)
+
+  let create head args =
+    let sorted_args =
+      List.sort_uniq (fun (name1, _) (name2, _) -> compare name1 name2) args
+    in
+    let t = { head; args = sorted_args } in
+    if List.length args != List.length sorted_args then
+      Misc.fatal_errorf "Names of instance arguments must be unique:@ %a"
+        print t;
+    t
+
+  let unsafe_create_unchecked head args = { head; args }
+end
+
+let compare_arg_name (name1, _) (name2, _) = Name.compare name1 name2
+
+let rec list_similar f list1 list2 =
+  match list1, list2 with
+  | [], [] -> true
+  | a :: list1, b :: list2 -> f a b && list_similar f list1 list2
+  | (_ :: _), [] | [], (_ :: _) -> false
+
+module T0 : sig
+  type t = private {
+    head : string;
+    visible_args : (Name.t * t) list;
+    hidden_args : (Name.t * t) list;
+  }
+
+  include Identifiable.S with type t := t
+
+  val create : string -> (Name.t * t) list -> hidden_args:(Name.t * t) list -> t
+
+  val to_name : t -> Name.t
+end = struct
+  type t = {
+    head : string;
+    visible_args : (Name.t * t) list;
+    hidden_args : (Name.t * t) list;
+  }
+
+  include Identifiable.Make (struct
+    type nonrec t = t
+
+    let rec compare
+        ({ head = head1; visible_args = visible_args1; hidden_args = hidden_args1 } as t1)
+        ({ head = head2; visible_args = visible_args2; hidden_args = hidden_args2 } as t2) =
+      if t1 == t2 then 0
+      else
+        match String.compare head1 head2 with
+        | 0 -> begin
+            match List.compare compare_pairs visible_args1 visible_args2 with
+            | 0 -> List.compare compare_pairs hidden_args1 hidden_args2
+            | c -> c
+          end
+        | c -> c
+    and compare_pairs (param1, value1) (param2, value2) =
+      match Name.compare param1 param2 with
+      | 0 -> compare value1 value2
+      | c -> c
+
+    let equal t1 t2 = compare t1 t2 = 0
+
+    let rec equal_looking t name =
+      let { head; visible_args; hidden_args } = t in
+      let { Name.head = name_head; args = name_args } = name in
+      hidden_args = []
+      && String.equal head name_head
+      && list_similar equal_looking_args visible_args name_args
+    and equal_looking_args (name1, value1) (name2, value2) =
+      Name.equal name1 name2 && equal_looking value1 value2
+
+    let rec print ppf { head; visible_args; hidden_args } =
+      Format.fprintf ppf "@[<hov 1>%s%a%a@]"
+        head
+        (pp_concat print_visible_pair) visible_args
+        (pp_concat print_hidden_pair) hidden_args
+    and print_visible_pair ppf (name, value) =
+      Format.fprintf ppf "[%a:%a]" Name.print name print value
+    and print_hidden_pair ppf (name, value) =
+      if equal_looking value name then
+        Format.fprintf ppf "{%a}" Name.print name
+      else
+        Format.fprintf ppf "{%a:%a}" Name.print name print value
+
+    let output = print |> Misc.output_of_print
+
+    let hash = Hashtbl.hash
+  end)
+
+  let create head visible_args ~hidden_args =
+    let visible_args_sorted = List.sort compare_arg_name visible_args in
+    let hidden_args_sorted = List.sort compare_arg_name hidden_args in
+    let t =
+      {
+        head;
+        visible_args = visible_args_sorted;
+        hidden_args = hidden_args_sorted;
+      }
+    in
+    if
+      List.length visible_args != List.length visible_args_sorted
+      || List.length hidden_args != List.length hidden_args_sorted
+    then
+      Misc.fatal_errorf "Names of arguments and parameters must be unique:@ %a"
+        print t;
+    t
+
+  (* CR-someday lmaurer: Should try and make this unnecessary or at least cheap.
+     Could do it by making [Name.t] an unboxed existential so that converting from
+     [t] is the identity. Or just have [Name.t] wrap [t] and ignore [hidden_args]. *)
+  let rec to_name ({ head; visible_args; hidden_args = _ }) : Name.t =
+    (* Safe because we already checked the names in this exact argument list *)
+    Name.unsafe_create_unchecked head (List.map arg_to_name visible_args)
+  and arg_to_name (name, value) =
+    name, to_name value
+end
+
+include T0
+
+let all_args t = t.visible_args @ t.hidden_args
+
+module Subst = Name.Map
+type subst = t Subst.t
+
+let rec subst0 (t : t) (s : subst) ~changed =
+  match Subst.find_opt (to_name t) s with
+  | Some rhs -> changed := true; rhs
+  | None -> subst0_inside t s ~changed
+and subst0_inside { head; visible_args; hidden_args } s ~changed =
+  let matching_hidden_args, non_matching_hidden_args =
+    List.partition_map
+      (fun ((name, value) as pair) ->
+          match Subst.find_opt (to_name value) s with
+          | Some rhs -> changed := true; Left (name, rhs)
+          | None -> Right pair)
+      hidden_args
+  in
+  let visible_args = subst0_alist visible_args s ~changed in
+  let hidden_args = subst0_alist non_matching_hidden_args s ~changed in
+  let visible_args =
+    List.merge compare_arg_name visible_args matching_hidden_args
+  in
+  create head visible_args ~hidden_args
+and subst0_alist l s ~changed =
+  List.map (fun (name, value) -> name, subst0 value s ~changed) l
+
+let subst t s =
+  let changed = ref false in
+  let new_t = subst0 t s ~changed in
+  if !changed then new_t, `Changed else t, `Did_not_change
+
+let subst_inside t s =
+  let changed = ref false in
+  let new_t = subst0_inside t s ~changed in
+  if !changed then new_t else t
+
+let check s args =
+  (* This could do more - say, check that the replacement (the argument) has
+      all the parameters of the original (the parameter). (The subset rule
+      requires this, since an argument has to refer to the parameter it
+      implements, and thus the parameter's parameters must include the
+      argument's parameters.) It would be redundant with the checks
+      implemented elsewhere but could still be helpful. *)
+  let param_set = List.map to_name args |> Name.Set.of_list in
+  Name.Set.subset (Name.Map.keys s) param_set
+
+let rec is_complete t =
+  match t.hidden_args with
+  | [] -> List.for_all (fun (_, value) -> is_complete value) t.visible_args
+  | _ -> false
+
+let has_arguments t =
+  match t with
+  | { head = _; visible_args = []; hidden_args = [] } -> false
+  | _ -> true
diff --git a/typing/global_module.mli b/typing/global_module.mli
new file mode 100644
index 00000000000..3f77c7918c1
--- /dev/null
+++ b/typing/global_module.mli
@@ -0,0 +1,100 @@
+[@@@ocaml.warning "+a-9-40-41-42"]
+
+module Name : sig
+  type t = private {
+    head : string;
+    args : (t * t) list;
+  }
+
+  include Identifiable.S with type t := t
+
+  val create : string -> (t * t) list -> t
+end
+
+(** An elaborated form of name in which all arguments are expressed, including
+    those being passed implicitly from one module to another by the subset rule
+    for parameterised modules. Normally, these "hidden" arguments simply say to
+    pass [X] as [X] for some module [X], but if there are parameterised
+    parameters, the hidden arguments can get more complex.
+
+    Suppose [M] takes parameters [X] and [Y], neither of which is itself
+    parameterised. If someone is passing [Foo] as the value of [X], then, we
+    will have (abbreviating nested records):
+
+    {v
+      { head: M; visible_args: [ X, Foo ]; hidden_args: [ Y, Y ] }
+    v}
+
+    This represents that [X] is explicitly being given the value [Foo] and [Y]
+    (the parameter) is implicitly getting the value [Y] (the argument currently
+    in scope).
+
+    However, suppose instead [Y] is parameterised by [X]. Then [M] still takes
+    two parameters [X] and [Y], but now once [X] has the value [Foo], [Y]
+    requires _that particular_ [X]:
+
+    {v
+      { head: M; visible_args: [ X, Foo ]; hidden_args: [ Y, Y[X:Foo] ] }
+    v}
+
+    Importantly, the _parameters_ [X] and [Y] never change: they are names that
+    appear in [m.ml] and [m.cmi]. But further specialisation requires passing
+    specifically a [Y[X:Foo]] rather than a [Y]. (Here, [Y[X:Foo]] stands for
+    the record [{ head = Y; visible_args = [ X, Foo ]; hidden_args = [] }] of
+    type [t].)
+*)
+type t = private {
+  head : string;
+  visible_args : (Name.t * t) list;
+  hidden_args : (Name.t * t) list;
+}
+
+include Identifiable.S with type t := t
+
+val create : string -> (Name.t * t) list -> hidden_args:(Name.t * t) list -> t
+
+val to_name : t -> Name.t
+
+val all_args : t -> (Name.t * t) list
+
+(** A map from parameter names to their values. Hidden arguments aren't relevant
+    in the parameter names, so they're represented by [Name.t]s here. *)
+type subst = t Name.Map.t
+
+(** Apply a substitution to the given global. If it appears in the substitution
+    directly (that is, its [Name.t] form is a key in the map), this simply
+    performs a lookup. Otherwise, we perform a _revealing substitution_: if the
+    value of a hidden argument is a key in the substitution, the argument becomes
+    visible. Otherwise, substitution recurses into arguments (both hidden and
+    visible) as usual. See [global_test.ml] for examples. *)
+val subst : t -> subst -> t * [ `Changed | `Did_not_change ]
+
+(** Apply a substitution to the arguments and parameters in [t] but not to [t]
+    itself. Useful if [subst] is constructed from some parameter-argument pairs
+    and [t] is one of the parameters, since we want to handle any
+    interdependencies but the substitution applied to [t] itself is
+    uninterestingly just the corresponding value. *)
+val subst_inside : t -> subst -> t
+
+(** Check that a substitution is a valid (possibly partial) instantiation of
+    a module with the given parameter list. Each name being substituted must
+    appear in the list. *)
+val check : subst -> t list -> bool
+
+(** Returns [true] if [hidden_args] is empty and all argument values (if any)
+    are also complete. This is a stronger condition than full application, and
+    (unless the whole global is itself a parameter) it's equivalent to the
+    global being a static constant, since any parameters being used would have
+    to show up in a [hidden_args] somewhere. (Importantly, it's not possible
+    that a parameter is being used as an argument to a different parameter,
+    since a module can be declared to be an argument for up to one parameter.)
+
+    CR lmaurer: Make sure we're checking for the user redundantly passing an
+    parameter as an argument. This should be accepted and ignored, lest we
+    count the parameter as filled and consider something completely
+    instantiated. *)
+val is_complete : t -> bool
+
+(** Returns [true] if this name has at least one argument (either hidden or
+    visible). *)
+val has_arguments : t -> bool
diff --git a/utils/misc.ml b/utils/misc.ml
index 395898f0368..02b07b16d37 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -1089,6 +1089,16 @@ let print_see_manual ppf manual_section =
     (pp_print_list ~pp_sep:(fun f () -> pp_print_char f '.') pp_print_int)
     manual_section
 
+let output_of_print print =
+  let output out_channel t =
+    let ppf = Format.formatter_of_out_channel out_channel in
+    print ppf t;
+    (* Must flush the formatter immediately because it has a buffer separate
+       from the output channel's buffer *)
+    Format.pp_print_flush ppf ()
+  in
+  output
+
 
 type filepath = string
 
diff --git a/utils/misc.mli b/utils/misc.mli
index 946d53e53b6..04f8d790d58 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -624,6 +624,12 @@ val pp_two_columns :
 val print_see_manual : Format.formatter -> int list -> unit
 (** See manual section *)
 
+val output_of_print :
+  (Format.formatter -> 'a -> unit) -> out_channel -> 'a -> unit
+(** [output_of_print print] produces an output function from a pretty printer.
+    Note that naively using [Format.formatter_of_out_channel] typechecks but
+    doesn't work because it fails to flush the formatter. *)
+
 (** {1 Displaying configuration variables} *)
 
 val show_config_and_exit : unit -> unit