diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 42d0f6416702..ecb0be48ebfd 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -260,7 +260,7 @@ let rec check_mexpr env mse mp_mse res = match mse with
     let sign, delta = check_mexpr env f mp_mse res in
     let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
     let state = (Environ.universes env, Conversion.checked_universes) in
-    let _ : UGraph.t = Subtyping.check_subtypes state env mp (MPbound farg_id) farg_b in
+    let (_ : UGraph.t), _ = Subtyping.check_subtypes ~cache:Subtyping.Cache.empty state env mp (MPbound farg_id) farg_b in
     let mp_delta =
       let mb = lookup_module mp env in
       match mod_type mb with
@@ -302,7 +302,7 @@ let rec check_module env opac mp mb opacify =
     and mtb2 = mk_mtb (mod_type mb) delta_mb in
     let state = (Environ.universes env, Conversion.checked_universes) in
     let env = Modops.add_module mp (module_body_of_type mtb1) env in
-    let _ : UGraph.t = Subtyping.check_subtypes state env mp mp mtb2 in
+    let (_ : UGraph.t), _ = Subtyping.check_subtypes ~cache:Subtyping.Cache.empty state env mp mp mtb2 in
     ()
   in
   opac
diff --git a/doc/changelog/01-kernel/22281-include-self-subtyping-perf-Fixed.rst b/doc/changelog/01-kernel/22281-include-self-subtyping-perf-Fixed.rst
new file mode 100644
index 000000000000..6bedc9c7aea1
--- /dev/null
+++ b/doc/changelog/01-kernel/22281-include-self-subtyping-perf-Fixed.rst
@@ -0,0 +1,12 @@
+- **Fixed:**
+  quadratic compilation time of chains of ``<+`` over functor module
+  types (and, more generally, of repeated module subtyping checks
+  against a large accumulated signature): the "Include Self" subtyping
+  check now looks fields up in the environment on demand instead of
+  eagerly strengthening and indexing the whole accumulated signature,
+  and successful field checks are cached so that re-checking the same
+  fields (e.g. against every prefix of a chain, or on repeated
+  applications of the same functor) hits a fast path
+  (`#22281 <https://github.com/rocq-prover/rocq/pull/22281>`_,
+  fixes `#22279 <https://github.com/rocq-prover/rocq/issues/22279>`_,
+  written by Claude (Anthropic), for Jason Gross).
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b6745cb0ad92..6e73109c75fa 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -177,7 +177,7 @@ let rec check_with_def (cst, ustate) env struc (idl, wth) mp reso =
 
 (* [mp] is the ambient modpath of [struc],
    [new_mp] is the path of the module to replace [idl] with *)
-let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
+let rec check_with_mod (cst, ustate) cache env struc (idl,new_mp) mp reso =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> id, idl
@@ -192,14 +192,13 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
     if List.is_empty idl then
       (* Toplevel module definition *)
       let new_mb = lookup_module new_mp env in
-      let cst = match Mod_declarations.mod_expr old with
+      let cst, cache = match Mod_declarations.mod_expr old with
         | Abstract ->
           let mtb_old = module_type_of_module old in
-          let cst = Subtyping.check_subtypes (cst, ustate) env' new_mp (MPdot (mp, lab)) mtb_old in
-          cst
+          Subtyping.check_subtypes ~cache (cst, ustate) env' new_mp (MPdot (mp, lab)) mtb_old
         | Algebraic (MENoFunctor (MEident(mp'))) ->
           check_modpath_equiv env' new_mp mp';
-          cst
+          cst, cache
         | _ -> error_generative_module_expected lab
       in
       let mp' = MPdot (mp,lab) in
@@ -211,7 +210,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
          with the identity substitution accompanied by the new resolver*)
       let id_subst = map_mp mp' mp' subreso in
       let new_after = subst_structure id_subst mp after in
-      before @ (lab, SFBmodule new_mb') :: new_after, subreso, cst
+      before @ (lab, SFBmodule new_mb') :: new_after, subreso, cst, cache
     else
       (* Module definition of a sub-module *)
       let mp' = MPdot (mp,lab) in
@@ -222,17 +221,17 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
       begin match Mod_declarations.mod_expr old with
       | Abstract ->
         let struc = destr_nofunctor mp' (mod_type old) in
-        let struc', subreso, cst =
-          check_with_mod (cst, ustate) env' struc (idl,new_mp) mp' (mod_delta old)
+        let struc', subreso, cst, cache =
+          check_with_mod (cst, ustate) cache env' struc (idl,new_mp) mp' (mod_delta old)
         in
         let reso' = add_delta_resolver (mod_delta old) (upcast_delta_resolver mp' subreso) in
         let new_mb = replace_module_body struc' reso' old in
         let id_subst = map_mp mp' mp' reso' in
         let new_after = subst_structure id_subst mp after in
-        before @ (lab, SFBmodule new_mb) :: new_after, subreso, cst
+        before @ (lab, SFBmodule new_mb) :: new_after, subreso, cst, cache
       | Algebraic (MENoFunctor (MEident mp0)) ->
         let () = check_modpath_equiv env' new_mp (rebuild_mp mp0 idl) in
-        before@(lab,spec)::after, reso, cst
+        before@(lab,spec)::after, reso, cst, cache
       | _ -> error_generative_module_expected lab
       end
   with
@@ -241,41 +240,41 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
 type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code }
 type 'a vm_state = 'a * 'a vm_handler
 
-let check_with ustate vmstate env mp (sign,reso,cst,vm) = function
+let check_with ustate vmstate env mp (sign,reso,cst,vm,cache) = function
   | WithDef(idl, (c, ctx)) ->
     let struc = destr_nofunctor mp sign in
     let univs = match ctx with None -> Monomorphic | Some uctx -> Polymorphic uctx in
     let vm, bcode = vmstate.vm_handler env univs c vm in
     let body = { w_def = c; w_univs = univs; w_bytecode = bcode } in
     let struc', cst = check_with_def (cst, ustate) env struc (idl, body) mp reso in
-    NoFunctor struc', reso, cst, vm
+    NoFunctor struc', reso, cst, vm, cache
   | WithMod(idl,new_mp) ->
     let struc = destr_nofunctor mp sign in
-    let struc', subreso, cst = check_with_mod (cst, ustate) env struc (idl, new_mp) mp reso in
+    let struc', subreso, cst, cache = check_with_mod (cst, ustate) cache env struc (idl, new_mp) mp reso in
     let reso' = add_delta_resolver reso (upcast_delta_resolver mp subreso) in
-    NoFunctor struc', reso', cst, vm
+    NoFunctor struc', reso', cst, vm, cache
 
-let check_with_alg ustate vmstate env mp (sign, alg, reso, cst, vm) wd =
-  let struc, reso, cst, vm = check_with ustate vmstate env mp (sign, reso, cst, vm) wd in
-  struc, MEwith (alg, wd), reso, cst, vm
+let check_with_alg ustate vmstate env mp (sign, alg, reso, cst, vm, cache) wd =
+  let struc, reso, cst, vm, cache = check_with ustate vmstate env mp (sign, reso, cst, vm, cache) wd in
+  struc, MEwith (alg, wd), reso, cst, vm, cache
 
-let rec translate_apply ustate env inl mp subst (sign, reso, cst) args = match args with
+let rec translate_apply ustate env inl mp subst (sign, reso, cst, cache) args = match args with
 | [] ->
   let sign = subst_signature subst mp sign in
   let reso = subst_codom_delta_resolver subst reso in
-  (sign, reso, cst)
+  (sign, reso, cst, cache)
 | mp1 :: args ->
   let farg_id, farg_b, sign = destr_functor sign in
   let farg_b =
     if is_empty_subst subst then farg_b
     else subst_modtype subst_codom subst (MPbound farg_id) farg_b
   in
-  let cst = Subtyping.check_subtypes (cst, ustate) env mp1 (MPbound farg_id) farg_b in
+  let cst, cache = Subtyping.check_subtypes ~direct:true ~cache (cst, ustate) env mp1 (MPbound farg_id) farg_b in
   let mp_delta = discr_resolver mp1 (lookup_module mp1 env) in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
   let nsubst = map_mbid farg_id mp1 mp_delta in
   let subst = join subst nsubst in
-  translate_apply ustate env inl mp subst (sign, reso, cst) args
+  translate_apply ustate env inl mp subst (sign, reso, cst, cache) args
 
 (** Translation of a module struct entry :
     - We translate to a module when a [module_path] is given,
@@ -288,7 +287,7 @@ let rec decompose_apply accu = function
 | MEapply (f, arg) -> decompose_apply (arg :: accu) f
 | (MEident _ | MEwith _) as f -> f, accu
 
-let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl me = match me with
+let rec translate_mse (cst, ustate) cache (vm, vmstate) env mpo inl me = match me with
   | MEident mp1 ->
     let mb = match mpo with
       | Some mp -> strengthen_and_subst_module_body mp1 (lookup_module mp1 env) mp false
@@ -296,59 +295,59 @@ let rec translate_mse (cst, ustate) (vm, vmstate) env mpo inl me = match me with
         let mt = lookup_modtype mp1 env in
         module_body_of_type mt
     in
-    mod_type mb, me, mod_delta mb, cst, vm
+    mod_type mb, me, mod_delta mb, cst, vm, cache
   | MEapply _ ->
     let fe, args = decompose_apply [] me in
-    let (sign, alg, reso, cst, vm) = translate_mse (cst, ustate) (vm, vmstate) env mpo inl fe in
+    let (sign, alg, reso, cst, vm, cache) = translate_mse (cst, ustate) cache (vm, vmstate) env mpo inl fe in
     let mp = match mpo with Some mp -> mp | None -> mp_from_mexpr fe in
-    let (sign, reso, cst) = translate_apply ustate env inl mp empty_subst (sign, reso, cst) args in
+    let (sign, reso, cst, cache) = translate_apply ustate env inl mp empty_subst (sign, reso, cst, cache) args in
     let alg = List.fold_left (fun accu arg -> MEapply (accu, arg)) alg args in
-    (sign, alg, reso, cst, vm)
+    (sign, alg, reso, cst, vm, cache)
   | MEwith(me, with_decl) ->
     assert (Option.is_empty mpo); (* No 'with' syntax for modules *)
     let mp = mp_from_mexpr me in
-    check_with_alg ustate vmstate env mp (translate_mse (cst, ustate) (vm, vmstate) env None inl me) with_decl
+    check_with_alg ustate vmstate env mp (translate_mse (cst, ustate) cache (vm, vmstate) env None inl me) with_decl
 
 let mk_modtype = Mod_declarations.make_module_type
 
-let rec translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod mp inl mse = function
+let rec translate_mse_funct (cst, ustate) cache (vm, vmstate) env ~is_mod mp inl mse = function
   | [] ->
-    let sign,alg,reso,cst,vm = translate_mse (cst, ustate) (vm, vmstate) env (if is_mod then Some mp else None) inl mse in
+    let sign,alg,reso,cst,vm,cache = translate_mse (cst, ustate) cache (vm, vmstate) env (if is_mod then Some mp else None) inl mse in
     let sign,reso =
       if is_mod then sign,reso
       else subst_modtype_signature_and_resolver (mp_from_mexpr mse) mp sign reso in
-    sign, MENoFunctor alg, reso, cst, vm
+    sign, MENoFunctor alg, reso, cst, vm, cache
   | (mbid, ty, ty_inl) :: params ->
     let mp_id = MPbound mbid in
-    let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp_id ty_inl ([],ty) in
+    let mtb, cst, vm, cache = translate_modtype (cst, ustate) cache (vm, vmstate) env mp_id ty_inl ([],ty) in
     let env' = add_module_parameter mbid mtb env in
-    let sign,alg,reso,cst,vm = translate_mse_funct (cst, ustate) (vm, vmstate) env' ~is_mod mp inl mse params in
+    let sign,alg,reso,cst,vm,cache = translate_mse_funct (cst, ustate) cache (vm, vmstate) env' ~is_mod mp inl mse params in
     let alg' = MEMoreFunctor alg in
-    MoreFunctor (mbid, mtb, sign), alg',reso, cst, vm
+    MoreFunctor (mbid, mtb, sign), alg',reso, cst, vm, cache
 
-and translate_modtype state vmstate env mp inl (params,mte) =
-  let sign,alg,reso,cst,vm = translate_mse_funct state vmstate env ~is_mod:false mp inl mte params in
+and translate_modtype state cache vmstate env mp inl (params,mte) =
+  let sign,alg,reso,cst,vm,cache = translate_mse_funct state cache vmstate env ~is_mod:false mp inl mte params in
   let mtb = mk_modtype sign reso in
-  set_algebraic_type mtb alg, cst, vm
+  set_algebraic_type mtb alg, cst, vm, cache
 
 (** [finalize_module] :
     from an already-translated (or interactive) implementation and
     an (optional) signature entry, produces a final [module_body] *)
 
-let finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sign,alg,reso) restype = match restype with
+let finalize_module_alg (cst, ustate) cache (vm, vmstate) env mp (sign,alg,reso) restype = match restype with
   | None ->
     let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
     let mb = make_module_body sign reso in
     let mb = set_implementation impl mb in
-    mb, cst, vm
+    mb, cst, vm, cache
   | Some (params_mte,inl) ->
-    let res_mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl params_mte in
+    let res_mtb, cst, vm, cache = translate_modtype (cst, ustate) cache (vm, vmstate) env mp inl params_mte in
     let auto_mtb = Mod_declarations.make_module_body sign reso in
     (* This function is supposed to be called in a state where the current module
        is about to be closed, so all subcomponents of the module are already
        part of the environment. We only need to add the toplevel module entry. *)
     let env = Environ.shallow_add_module mp auto_mtb env in
-    let cst = Subtyping.check_subtypes (cst, ustate) env mp mp res_mtb in
+    let cst, cache = Subtyping.check_subtypes ~direct:true ~cache (cst, ustate) env mp mp res_mtb in
     let impl = match alg with
     | Some e -> Algebraic e
     | None ->
@@ -363,24 +362,25 @@ let finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sign,alg,reso) resty
     mb,
     (** constraints from module body typing + subtyping + module type. *)
     cst,
-    vm
+    vm,
+    cache
 
-let finalize_module univs vm env mp (sign, reso) typ =
-  finalize_module_alg univs vm env mp (sign, None, reso) typ
+let finalize_module univs cache vm env mp (sign, reso) typ =
+  finalize_module_alg univs cache vm env mp (sign, None, reso) typ
 
-let translate_module (cst, ustate) (vm, vmstate) env mp inl = function
+let translate_module (cst, ustate) cache (vm, vmstate) env mp inl = function
   | MType (params,ty) ->
-    let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl (params,ty) in
-    module_body_of_type mtb, cst, vm
+    let mtb, cst, vm, cache = translate_modtype (cst, ustate) cache (vm, vmstate) env mp inl (params,ty) in
+    module_body_of_type mtb, cst, vm, cache
   | MExpr (params,mse,oty) ->
-    let (sg,alg,reso,cst,vm) = translate_mse_funct (cst, ustate) (vm, vmstate) env ~is_mod:true mp inl mse params in
+    let (sg,alg,reso,cst,vm,cache) = translate_mse_funct (cst, ustate) cache (vm, vmstate) env ~is_mod:true mp inl mse params in
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
     (* finalize_module_alg expects the subcomponents to be part of the environment *)
     let env = match sg with
     | NoFunctor struc -> Modops.add_structure mp struc reso env
     | MoreFunctor _ -> env
     in
-    finalize_module_alg (cst, ustate) (vm, vmstate) env mp (sg,Some alg,reso) restype
+    finalize_module_alg (cst, ustate) cache (vm, vmstate) env mp (sg,Some alg,reso) restype
 
 (** We now forbid any Include of functors with restricted signatures.
     Otherwise, we could end with the creation of undesired axioms
@@ -409,23 +409,23 @@ let rec forbid_incl_signed_functor env = function
       forbid_incl_signed_functor env me
     | _ -> ()
 
-let rec translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl = function
+let rec translate_mse_include_module (cst, ustate) cache (vm, vmstate) env mp inl = function
   | MEident mp1 ->
     let mb = strengthen_and_subst_module_body mp1 (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr (mod_type mb) in
-    sign, (), mod_delta mb, cst, vm
+    sign, (), mod_delta mb, cst, vm, cache
   | MEapply _ as me ->
     let fe, args = decompose_apply [] me in
-    let (sign, (), reso, cst, vm) = translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl fe in
-    let (sign, reso, cst) = translate_apply ustate env inl mp empty_subst (sign, reso, cst) args in
-    (sign, (), reso, cst, vm)
+    let (sign, (), reso, cst, vm, cache) = translate_mse_include_module (cst, ustate) cache (vm, vmstate) env mp inl fe in
+    let (sign, reso, cst, cache) = translate_apply ustate env inl mp empty_subst (sign, reso, cst, cache) args in
+    (sign, (), reso, cst, vm, cache)
   | MEwith _ -> assert false (* No 'with' syntax for modules *)
 
-let translate_mse_include is_mod (cst, ustate) (vm, vmstate) env mp inl me =
+let translate_mse_include is_mod (cst, ustate) cache (vm, vmstate) env mp inl me =
   if is_mod then
     let () = forbid_incl_signed_functor env me in
-    translate_mse_include_module (cst, ustate) (vm, vmstate) env mp inl me
+    translate_mse_include_module (cst, ustate) cache (vm, vmstate) env mp inl me
   else
-    let mtb, cst, vm = translate_modtype (cst, ustate) (vm, vmstate) env mp inl ([],me) in
+    let mtb, cst, vm, cache = translate_modtype (cst, ustate) cache (vm, vmstate) env mp inl ([],me) in
     let sign = clean_bounded_mod_expr (mod_type mtb) in
-    sign, (), mod_delta mtb, cst, vm
+    sign, (), mod_delta mtb, cst, vm, cache
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 95f8863b10a0..60db552b93ee 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -20,6 +20,11 @@ open Names
 type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code }
 type 'a vm_state = 'a * 'a vm_handler
 
+(** Each translation function below additionally threads a
+    [Subtyping.Cache.t] of the subtyping field checks it performed (see
+    {!Subtyping.Cache} for the conditions under which the caller may
+    reuse the returned cache). *)
+
 (** [translate_module] produces a [module_body] out of a [module_entry].
     In the output fields:
     - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
@@ -28,30 +33,33 @@ type 'a vm_state = 'a * 'a vm_handler
 
 val translate_module :
   ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
+  Subtyping.Cache.t ->
   'b vm_state ->
-  env -> ModPath.t -> inline -> module_entry -> module_body * 'a * 'b
+  env -> ModPath.t -> inline -> module_entry -> module_body * 'a * 'b * Subtyping.Cache.t
 
 (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
     cannot be [None] (and of course [mod_expr] is [Abstract]). *)
 
 val translate_modtype :
   ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
+  Subtyping.Cache.t ->
   'b vm_state ->
-  env -> ModPath.t -> inline -> module_type_entry -> module_type_body * 'a * 'b
+  env -> ModPath.t -> inline -> module_type_entry -> module_type_body * 'a * 'b * Subtyping.Cache.t
 
 (** From an already-translated (or interactive) implementation and
     an (optional) signature entry, produces a final [module_body] *)
 
 val finalize_module :
   ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
+  Subtyping.Cache.t ->
   'b vm_state ->
   env -> ModPath.t -> module_signature * delta_resolver ->
   (module_type_entry * inline) option ->
-  module_body * 'a * 'b
+  module_body * 'a * 'b * Subtyping.Cache.t
 
 (** [translate_mse_incl] translate the mse of a module or
     module type given to an Include *)
 
 val translate_mse_include :
-  bool -> ('a, Conversion.graph_inconsistency) Conversion.universe_state -> 'b vm_state -> Environ.env -> ModPath.t -> inline ->
-  module_struct_entry -> module_signature * unit * delta_resolver * 'a * 'b
+  bool -> ('a, Conversion.graph_inconsistency) Conversion.universe_state -> Subtyping.Cache.t -> 'b vm_state -> Environ.env -> ModPath.t -> inline ->
+  module_struct_entry -> module_signature * unit * delta_resolver * 'a * 'b * Subtyping.Cache.t
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 70f0b8c3bae1..db001eda04fd 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -59,6 +59,16 @@ val add_retroknowledge : Retroknowledge.action list -> env -> env
 
 val strengthen : module_type_body -> ModPath.t -> module_type_body
 
+(** Strengthening of a single constant field [l] of the module [mp], w.r.t.
+    the delta resolver of that module. Used to strengthen fields on demand
+    instead of strengthening a whole signature eagerly. *)
+val strengthen_const :
+  ModPath.t -> Id.t -> constant_body -> delta_resolver -> constant_body
+
+(** Strengthening of a single module field of a signature, as performed on
+    submodules by [strengthen]. *)
+val strengthen_module : ModPath.t -> module_body -> module_body
+
 val strengthen_and_subst_module_body : ModPath.t -> module_body -> ModPath.t -> bool -> module_body
 
 val subst_modtype_signature_and_resolver : ModPath.t -> ModPath.t ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index dbcbecf77cf5..bc0ba2180817 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -236,6 +236,12 @@ type safe_environment =
     loads : (ModPath.t * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
     opaquetab : Opaqueproof.opaquetab;
+    subtyping_cache : Subtyping.Cache.t;
+    (** Module subtyping checks already performed in (an earlier state
+        of) [env]. Storing the cache inside the safe environment ensures
+        it never outlives the monotonic evolution of [env] that cached
+        verdicts rely on: discarding or rolling back the safe
+        environment also discards the cache (see {!Subtyping.Cache}). *)
 }
 
 and modvariant =
@@ -268,6 +274,7 @@ let empty_environment =
     loads = [];
     local_retroknowledge = [];
     opaquetab = Opaqueproof.empty_opaquetab;
+    subtyping_cache = Subtyping.Cache.empty;
 }
 
 let is_initial senv =
@@ -1361,7 +1368,8 @@ let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let state = check_state senv in
   let vmstate = vm_state senv in
-  let mtb, _, vmtab = Mod_typing.translate_modtype state vmstate senv.env mp inl params_mte  in
+  let mtb, _, vmtab, cache = Mod_typing.translate_modtype state senv.subtyping_cache vmstate senv.env mp inl params_mte  in
+  let senv = { senv with subtyping_cache = cache } in
   let senv = set_vm_library vmtab senv in
   let mtb = Mod_declarations.hcons_module_type mtb in
   let senv = add_field (l,SFBmodtype mtb) (MT mp) senv in
@@ -1373,7 +1381,8 @@ let add_module l me inl senv =
   let mp = MPdot(senv.modpath, l) in
   let state = check_state senv in
   let vmstate = vm_state senv in
-  let mb, _, vmtab = Mod_typing.translate_module state vmstate senv.env mp inl me in
+  let mb, _, vmtab, cache = Mod_typing.translate_module state senv.subtyping_cache vmstate senv.env mp inl me in
+  let senv = { senv with subtyping_cache = cache } in
   let senv = set_vm_library vmtab senv in
   let mb = Mod_declarations.hcons_module_body mb in
   let senv = add_field (l,SFBmodule mb) (M mp) senv in
@@ -1405,6 +1414,7 @@ let start_mod_modtype ~istype l senv =
     elims = senv.elims;
     required = senv.required;
     opaquetab = senv.opaquetab;
+    subtyping_cache = senv.subtyping_cache;
     sections = None; (* checked in check_empty_context *)
 
     (* module local fields *)
@@ -1427,7 +1437,8 @@ let add_module_parameter mbid mte inl senv =
   let mp = MPbound mbid in
   let state = check_state senv in
   let vmstate = vm_state senv in
-  let mtb, _, vmtab = Mod_typing.translate_modtype state vmstate senv.env mp inl ([],mte) in
+  let mtb, _, vmtab, cache = Mod_typing.translate_modtype state senv.subtyping_cache vmstate senv.env mp inl ([],mte) in
+  let senv = { senv with subtyping_cache = cache } in
   let senv = set_vm_library vmtab senv in
   let senv = { senv with env = Modops.add_module_parameter mbid mtb senv.env } in
   let new_variant = match senv.modvariant with
@@ -1480,12 +1491,12 @@ let build_module_body params restype senv =
   let state = check_state senv in
   let vmstate = vm_state senv in
   (* XXX why are we dropping vmtab here? *)
-  let mb, _, _vmtab =
-    Mod_typing.finalize_module state vmstate senv.env senv.modpath
+  let mb, _, _vmtab, cache =
+    Mod_typing.finalize_module state senv.subtyping_cache vmstate senv.env senv.modpath
       (struc, senv.modresolver) restype'
   in
   let mb' = functorize_module params mb in
-  mb'
+  mb', cache
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -1513,6 +1524,9 @@ let propagate_senv newdef senv oldsenv =
     local_retroknowledge =
       senv.local_retroknowledge@oldsenv.local_retroknowledge;
     opaquetab = senv.opaquetab;
+    (* Ending a module keeps its fields and universes in the
+       environment, so verdicts cached inside it remain valid. *)
+    subtyping_cache = senv.subtyping_cache;
   }
 
 let end_module l restype senv =
@@ -1521,7 +1535,8 @@ let end_module l restype senv =
   let () = check_current_label l mp in
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
-  let mb = build_module_body params restype senv in
+  let mb, cache = build_module_body params restype senv in
+  let senv = { senv with subtyping_cache = cache } in
   let newenv = Environ.set_universes (Environ.universes senv.env) oldsenv.env in
   let newenv = Environ.set_qualities (Environ.qualities senv.env) newenv in
   let newenv = if Environ.rewrite_rules_allowed senv.env then Environ.allow_rewrite_rules newenv else newenv in
@@ -1562,29 +1577,31 @@ let add_include me is_module inl senv =
   let mp_sup = senv.modpath in
   let state = check_state senv in
   let vmstate = vm_state senv in
-  let sign,(),resolver, _, vmtab =
-    translate_mse_include is_module state vmstate senv.env mp_sup inl me
+  let sign,(),resolver, _, vmtab, cache =
+    translate_mse_include is_module state senv.subtyping_cache vmstate senv.env mp_sup inl me
   in
+  let senv = { senv with subtyping_cache = cache } in
   let senv = set_vm_library vmtab senv in
   (* Include Self support  *)
   let struc = NoFunctor (List.rev senv.revstruct) in
   let mb = Mod_declarations.make_module_body struc senv.modresolver in
-  let rec compute_sign sign resolver =
+  let rec compute_sign sign resolver cache =
     match sign with
     | MoreFunctor(mbid,mtb,str) ->
       let state = check_state senv in
       (* Module subcomponents are already part of senv.env at this point *)
       let env = Environ.shallow_add_module mp_sup mb senv.env in
-      let (_ : UGraph.t) = Subtyping.check_subtypes state env mp_sup (MPbound mbid) mtb in
+      let (_ : UGraph.t), cache = Subtyping.check_subtypes ~direct:true ~cache state env mp_sup (MPbound mbid) mtb in
       let mpsup_delta =
         Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb senv.modresolver
       in
       let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
       let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
-      compute_sign (Modops.subst_signature subst mp_sup str) resolver
-    | NoFunctor str -> resolver, str
+      compute_sign (Modops.subst_signature subst mp_sup str) resolver cache
+    | NoFunctor str -> resolver, str, cache
   in
-  let resolver, str = compute_sign sign resolver in
+  let resolver, str, cache = compute_sign sign resolver senv.subtyping_cache in
+  let senv = { senv with subtyping_cache = cache } in
   let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv in
   let add senv ((l,elem) as field) =
     let new_name = match elem with
@@ -1639,6 +1656,7 @@ let start_library dir senv =
     loads = [];
     local_retroknowledge = [];
     opaquetab = Opaqueproof.empty_opaquetab;
+    subtyping_cache = senv.subtyping_cache;
   }
 
 let export ~output_native_objects senv dir =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0443f7b57682..9e88603bc753 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -66,14 +66,134 @@ type labmap = { objs : namedobject Id.Map.t; mods : namedmodule Id.Map.t }
 
 let empty_labmap = { objs = Id.Map.empty; mods = Id.Map.empty }
 
-let get_obj mp map l =
-  try Id.Map.find l map.objs
+(** How to look up the fields of the implementation (subtype) side of a
+    check.
+
+    [Direct] is used when the caller guarantees that the fields of the
+    module at [mp1] are part of the environment, unsubstituted — the
+    invariant documented in [check_structure] for [nargs = 0]: this holds
+    for the current interactive module (Include self), for any module
+    already added to the environment (functor application), and for a
+    module about to be closed. Fields are then looked up directly in the
+    environment, which avoids building a label map over the whole
+    signature when only a few fields are checked.
+
+    [Direct (Some reso)] additionally means that constant and submodule
+    fields must be seen strengthened w.r.t. [reso], producing the same
+    fields as looking them up in [Modops.strengthen] of the signature.
+    Strengthening of constants is performed on demand in [check_constant].
+
+    Lookups fall back to the label map (built lazily from the signature)
+    when the label does not correspond to a field of the module (e.g. the
+    name of a constructor or of a secondary inductive type of a block), so
+    behavior is unchanged in those cases. *)
+type direct_access =
+  | NoDirect
+  | Direct of Mod_subst.delta_resolver option
+
+type sigview = { sv_direct : direct_access; sv_map : labmap Lazy.t }
+
+let get_obj_fallback mp view l =
+  try Id.Map.find l (Lazy.force view.sv_map).objs
   with Not_found -> error_no_such_label_sub l (ModPath.to_string mp)
 
-let get_mod mp map l =
-  try Id.Map.find l map.mods
+let get_obj env mp view l =
+  match view.sv_direct with
+  | NoDirect -> get_obj_fallback mp view l
+  | Direct _ ->
+    (* strengthening of constants, when required, is done in [check_constant] *)
+    begin match Environ.lookup_constant_opt (Constant.make2 mp l) env with
+    | Some cb -> Constant cb
+    | None ->
+      let mind = MutInd.make2 mp l in
+      if Environ.mem_mind mind env then
+        let mib = Environ.lookup_mind mind env in
+        if Id.equal mib.mind_packets.(0).mind_typename l
+        then IndType ((mind, 0), mib)
+        else get_obj_fallback mp view l
+      else get_obj_fallback mp view l
+    end
+
+let get_mod_fallback mp view l =
+  try Id.Map.find l (Lazy.force view.sv_map).mods
   with Not_found -> error_no_such_label_sub l (ModPath.to_string mp)
 
+let get_mod env mp view l =
+  match view.sv_direct with
+  | NoDirect -> get_mod_fallback mp view l
+  | Direct str ->
+    let mp' = MPdot (mp, l) in
+    begin match Environ.lookup_module mp' env with
+    | mb ->
+      let mb = match str with
+        | Some _ -> Modops.strengthen_module mp' mb
+        | None -> mb
+      in
+      Module mb
+    | exception Not_found ->
+      match Environ.lookup_modtype mp' env with
+      | mtb -> Modtype mtb
+      | exception Not_found -> get_mod_fallback mp view l
+    end
+
+(** Cache of successful constant field checks.
+
+    A successful check of an implementation field [cb1] against an
+    expected field [cb2] is a function of the pair itself whenever both
+    substitutions leave the bodies physically unchanged (checked at run
+    time) and the check did not produce new universe constraints (the
+    returned state is physically the input one; the kernel-side checking
+    mode never produces constraints, and the inference mode returns its
+    input state unchanged when all needed constraints are already
+    entailed). Such a check stays valid later in the same process:
+    - the environment only grows, and a successful conversion is
+      preserved by adding constants, universe constraints or rewrite
+      rules (conversion success is monotone in the environment);
+    - constant bodies are immutable, and rolling back the environment
+      (Undo, Reset) also drops every object that could re-present the
+      cached pair;
+    - conversion compares constant references up to the delta resolver
+      (canonical names), so a successful check is independent of the
+      user-level path under which physically equal bodies are reached.
+
+    Cached verdicts are only valid as long as the ambient environment
+    evolves monotonically. The cache is therefore purely functional and
+    threaded through the checks: callers store it alongside the
+    environment their checks were performed in (a [safe_environment]
+    field on the kernel side), so that discarding or rolling back that
+    environment also discards or rolls back the cache.
+
+    The cache is indexed by the label of the field — whose hash is cheap,
+    and which is stable across the module paths under which the same
+    bodies may be rechecked (e.g. re-including a functor in each stage of
+    a chain of module types) — and holds a short list of successfully
+    checked pairs for that label, compared physically. The list is
+    capped, so the cache retains a bounded number of bodies per label
+    ever checked. Failures are not cached (they raise). *)
+module Cache =
+struct
+  type t = (constant_body * constant_body) list Id.Map.t
+
+  let empty = Id.Map.empty
+
+  let max_gen = 16
+
+  let mem l cb1 cb2 cache =
+    match Id.Map.find_opt l cache with
+    | None -> false
+    | Some pairs -> List.exists (fun (c1, c2) -> c1 == cb1 && c2 == cb2) pairs
+
+  let add l cb1 cb2 cache =
+    let prev = match Id.Map.find_opt l cache with
+      | None -> []
+      | Some pairs ->
+        if List.length pairs >= max_gen
+        then CList.firstn (max_gen - 1) pairs
+        else pairs
+    in
+    Id.Map.add l ((cb1, cb2) :: prev) cache
+end
+
 let make_labmap mp list =
   let add_one (l,e) map =
    match e with
@@ -247,7 +367,7 @@ let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 r
     cst
 
 
-let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 =
+let check_constant (cst, ustate) cache trace env mp1 l strengthen1 info1 cb2 subst1 subst2 =
   let error why = error_signature_mismatch trace l why in
   let check_conv why cst poly pb = check_conv_error error why (cst, ustate) poly pb in
   let check_type poly cst env t1 t2 =
@@ -256,17 +376,31 @@ let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 =
   in
   match info1 with
     | IndType _ | IndConstr _ | Rules -> error DefinitionFieldExpected
-    | Constant cb1 ->
-      let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
-      let cb1 = Declareops.subst_const_body subst1 cb1 in
-      let cb2 = Declareops.subst_const_body subst2 cb2 in
+    | Constant cb1_0 ->
+      let cb2_0 = cb2 in
+      let () = assert (List.is_empty cb1_0.const_hyps && List.is_empty cb2_0.const_hyps) in
+      (* On-demand strengthening (see [direct_access]) only happens with an
+         empty [subst1], so it commutes with the substitution below. *)
+      let () = assert (Option.is_empty strengthen1 || is_empty_subst subst1) in
+      let scb1 = Declareops.subst_const_body subst1 cb1_0 in
+      let scb2 = Declareops.subst_const_body subst2 cb2_0 in
+      (* The outcome only depends on the pair of bodies when both
+         substitutions leave them physically unchanged, see [Cache]. *)
+      let context_free = scb1 == cb1_0 && scb2 == cb2_0 in
+      if context_free && Cache.mem l cb1_0 cb2_0 cache then (cst, cache)
+      else begin
+      let cb1 = match strengthen1 with
+        | Some reso -> Modops.strengthen_const mp1 l scb1 reso
+        | None -> scb1
+      in
+      let cb2 = scb2 in
       (* Start by checking universes *)
       let env = check_universes error env cb1.const_universes cb2.const_universes in
       let poly = Declareops.constant_is_polymorphic cb1 in
       (* Now check types *)
       let typ1 = cb1.const_type in
       let typ2 = cb2.const_type in
-      let cst = check_type poly cst env typ1 typ2 in
+      let cst' = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
          - A transparent constant can only be implemented by a compatible
            transparent constant.
@@ -277,80 +411,95 @@ let check_constant (cst, ustate) trace env l info1 cb2 subst1 subst2 =
          - In the signature, an opaque is handled just as a parameter:
            anything of the right type can implement it, even if bodies differ.
       *)
-      (match cb2.const_body with
-       | Undef _ | OpaqueDef _ -> cst
-       | Primitive _ | Symbol _ -> error (NotConvertibleBodyField None)
-       | Def c2 ->
-         (match cb1.const_body with
-          | Primitive _ | Undef _ | OpaqueDef _ | Symbol _ -> error (NotConvertibleBodyField None)
-          | Def c1 ->
-            (* NB: cb1 might have been strengthened and appear as transparent.
-               Anyway [check_conv] will handle that afterwards. *)
-            check_conv (NotConvertibleBodyField (Some (env, c1, c2))) cst poly CONV env c1 c2))
-
-let rec check_modules state trace env mp1 msb1 mp2 msb2 subst1 subst2 =
+      let cst' =
+        (match cb2.const_body with
+         | Undef _ | OpaqueDef _ -> cst'
+         | Primitive _ | Symbol _ -> error (NotConvertibleBodyField None)
+         | Def c2 ->
+           (match cb1.const_body with
+            | Primitive _ | Undef _ | OpaqueDef _ | Symbol _ -> error (NotConvertibleBodyField None)
+            | Def c1 ->
+              (* NB: cb1 might have been strengthened and appear as transparent.
+                 Anyway [check_conv] will handle that afterwards. *)
+              check_conv (NotConvertibleBodyField (Some (env, c1, c2))) cst' poly CONV env c1 c2))
+      in
+      (* Only cache checks that produced no new universe constraints: they
+         are then pure and stay valid as long as the environment the cache
+         is stored alongside evolves monotonically. *)
+      let cache =
+        if context_free && cst' == cst then Cache.add l cb1_0 cb2_0 cache
+        else cache
+      in
+      (cst', cache)
+      end
+
+let rec check_modules state cache trace env mp1 msb1 mp2 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in
   let mty2 = module_type_of_module msb2 in
-  check_modtypes state trace env mp1 mty1 mp2 mty2 subst1 subst2
+  check_modtypes state cache trace env mp1 mty1 mp2 mty2 subst1 subst2
 
-and check_signatures (cst, ustate) trace env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2 =
-  let map1 = make_labmap mp1 sig1 in
-  let check_one_body cst (l,spec2) =
+and check_signatures (cst, ustate) cache trace env mp1 sig1 dir mp2 sig2 subst1 subst2 reso1 reso2 =
+  let view = { sv_direct = dir; sv_map = lazy (make_labmap mp1 sig1) } in
+  let strengthen1 = match dir with Direct str -> str | NoDirect -> None in
+  let check_one_body (cst, cache) (l,spec2) =
     match spec2 with
         | SFBconst cb2 ->
-            check_constant (cst, ustate) trace env l (get_obj mp1 map1 l)
+            check_constant (cst, ustate) cache trace env mp1 l strengthen1 (get_obj env mp1 view l)
               cb2 subst1 subst2
         | SFBmind mib2 ->
-            check_inductive (cst, ustate) trace env mp1 l (get_obj mp1 map1 l)
-              mp2 mib2 subst1 subst2 reso1 reso2
+            check_inductive (cst, ustate) trace env mp1 l (get_obj env mp1 view l)
+              mp2 mib2 subst1 subst2 reso1 reso2,
+            cache
         | SFBrules _ ->
             error_signature_mismatch trace l NoRewriteRulesSubtyping
         | SFBmodule msb2 ->
             let mp1' = MPdot (mp1, l) in
             let mp2' = MPdot (mp2, l) in
-            begin match get_mod mp1 map1 l with
-              | Module msb1 -> check_modules (cst, ustate) (Submodule l :: trace) env mp1' msb1 mp2' msb2 subst1 subst2
+            begin match get_mod env mp1 view l with
+              | Module msb1 -> check_modules (cst, ustate) cache (Submodule l :: trace) env mp1' msb1 mp2' msb2 subst1 subst2
               | _ -> error_signature_mismatch trace l ModuleFieldExpected
             end
         | SFBmodtype mtb2 ->
-            let mtb1 = match get_mod mp1 map1 l with
+            let mtb1 = match get_mod env mp1 view l with
               | Modtype mtb -> mtb
               | _ -> error_signature_mismatch trace l ModuleTypeFieldExpected
             in
             let mp1' = MPdot (mp1, l) in
             let mp2' = MPdot (mp2, l) in
             (* Check for equivalence via subtyping in both directions *)
-            let cst =
+            let cst, cache =
               let env = add_module mp1' (module_body_of_type mtb1) env in
-              check_modtypes (cst, ustate) (Submodule l :: trace) env mp1' mtb1 mp2' mtb2 subst1 subst2
+              check_modtypes (cst, ustate) cache (Submodule l :: trace) env mp1' mtb1 mp2' mtb2 subst1 subst2
             in
             let env = add_module mp2' (module_body_of_type mtb2) env in
-            check_modtypes (cst, ustate) (Submodule l :: trace) env mp2' mtb2 mp1' mtb1 subst2 subst1
+            check_modtypes (cst, ustate) cache (Submodule l :: trace) env mp2' mtb2 mp1' mtb1 subst2 subst1
   in
-    List.fold_left check_one_body cst sig2
+    List.fold_left check_one_body (cst, cache) sig2
 
-and check_modtypes (cst, ustate) trace env mp1 mtb1 mp2 mtb2 subst1 subst2 =
-  if mtb1==mtb2 || mod_type mtb1 == mod_type mtb2 then cst
+and check_modtypes ?(dir=NoDirect) (cst, ustate) cache trace env mp1 mtb1 mp2 mtb2 subst1 subst2 =
+  if mtb1==mtb2 || mod_type mtb1 == mod_type mtb2 then (cst, cache)
   else
-    let rec check_structure cst ~nargs env struc1 struc2 subst1 subst2 =
+    let rec check_structure (cst, cache) ~nargs env struc1 struc2 subst1 subst2 =
       match struc1,struc2 with
       | NoFunctor list1,
         NoFunctor list2 ->
-        let env =
+        let env, dir =
           if Int.equal nargs 0 then
             (* Not a functor, so the body and all its subcomponents should
                already be in the environment *)
-            env
+            env, dir
           else
             (* We only add the subcomponents, the functor per se is already
                part of the environment but the subtyping check will never access
-               it directly *)
-            Modops.add_structure mp1 (subst_structure subst1 mp1 list1) (mod_delta mtb1) env
+               it directly.  The fields added to the environment are
+               substituted, so direct access does not apply to them. *)
+            Modops.add_structure mp1 (subst_structure subst1 mp1 list1) (mod_delta mtb1) env,
+            NoDirect
         in
         let delta_mtb1 = mod_delta mtb1 in
         let delta_mtb2 = mod_delta mtb2 in
-        check_signatures (cst, ustate) trace env
-          mp1 list1 mp2 list2 subst1 subst2
+        check_signatures (cst, ustate) cache trace env
+          mp1 list1 dir mp2 list2 subst1 subst2
           delta_mtb1 delta_mtb2
       | MoreFunctor (arg_id1,arg_t1,body_t1),
         MoreFunctor (arg_id2,arg_t2,body_t2) ->
@@ -358,18 +507,27 @@ and check_modtypes (cst, ustate) trace env mp1 mtb1 mp2 mtb2 subst1 subst2 =
         let mparg2 = MPbound arg_id2 in
         let subst1 = join (map_mbid arg_id1 mparg2 (mod_delta arg_t2)) subst1 in
         let env = add_module_parameter arg_id2 arg_t2 env in
-        let cst = check_modtypes (cst, ustate) (FunctorArgument (nargs+1) :: trace) env mparg2 arg_t2 mparg1 arg_t1 subst2 subst1 in
+        let cst, cache = check_modtypes (cst, ustate) cache (FunctorArgument (nargs+1) :: trace) env mparg2 arg_t2 mparg1 arg_t1 subst2 subst1 in
         (* contravariant *)
-        check_structure cst ~nargs:(nargs + 1) env body_t1 body_t2 subst1 subst2
+        check_structure (cst, cache) ~nargs:(nargs + 1) env body_t1 body_t2 subst1 subst2
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2
     in
-    check_structure cst ~nargs:0 env (mod_type mtb1) (mod_type mtb2) subst1 subst2
+    check_structure (cst, cache) ~nargs:0 env (mod_type mtb1) (mod_type mtb2) subst1 subst2
 
-let check_subtypes state env mp_sup mp_super super =
+let check_subtypes ?(direct=false) ~cache state env mp_sup mp_super super =
   let sup = match Environ.lookup_module mp_sup env with
   | mb -> module_type_of_module mb
   | exception Not_found -> assert false
   in
-  check_modtypes state [] env
-    mp_sup (strengthen sup mp_sup) mp_super super empty_subst
-    (map_mp mp_super mp_sup (mod_delta sup))
+  let subst2 = map_mp mp_super mp_sup (mod_delta sup) in
+  if direct then
+    (* The caller guarantees that the fields of [mp_sup] are in [env],
+       unsubstituted; look them up there on demand instead of eagerly
+       strengthening the whole signature (see [direct_access]).
+       [mod_global_delta] is [None] on functors, where [strengthen] does
+       not strengthen either. *)
+    let dir = Direct (mod_global_delta sup) in
+    check_modtypes ~dir (state) cache [] env mp_sup sup mp_super super empty_subst subst2
+  else
+    check_modtypes state cache [] env
+      mp_sup (strengthen sup mp_sup) mp_super super empty_subst subst2
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 15d8f1378bc1..8e44a1e3ac17 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -12,7 +12,33 @@ open Names
 open Mod_declarations
 open Environ
 
-val check_subtypes : ('a, Conversion.graph_inconsistency) Conversion.universe_state -> env -> ModPath.t -> ModPath.t -> module_type_body -> 'a
+(** Purely functional cache of successful field subtype checks.
+
+    Cached verdicts remain valid as long as the environment the checks
+    were performed in evolves monotonically. Callers are expected to
+    store the cache alongside that environment (e.g. as a field of the
+    kernel's [safe_environment], or in a state summary), so that
+    discarding or rolling back the environment also discards or rolls
+    back the cache — the cache must not outlive the environment. *)
+module Cache :
+sig
+  type t
+  val empty : t
+end
+
+(** [check_subtypes ~cache state env mp_sub mp_super super] checks that
+    the module at [mp_sub] has a type which is a subtype of [super]
+    (expected to live at [mp_super]), and returns the given cache
+    augmented with the field checks performed.
+
+    [direct] may be set when the fields of the module at [mp_sub] are part
+    of [env], unsubstituted — e.g. the current interactive module, a module
+    already added to the environment, or a module about to be closed. The
+    fields are then looked up in the environment on demand instead of
+    walking (and strengthening) the whole signature eagerly, which makes the
+    check proportional to the size of [super] instead of the size of the
+    subtype's signature. *)
+val check_subtypes : ?direct:bool -> cache:Cache.t -> ('a, Conversion.graph_inconsistency) Conversion.universe_state -> env -> ModPath.t -> ModPath.t -> module_type_body -> 'a * Cache.t
 
 val check_polymorphic_universes :
   Environ.env ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e1e4e59ecbc0..52ec01fdd95f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -194,7 +194,7 @@ let expand_mexpr env mp me =
      name that should not be part of the env and then substitute it away *)
   let mp0 = ModPath.dummy in
   let state = ((Environ.universes env, Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let mb, (_, cst), _ = Mod_typing.translate_module state vm_state env mp0 inl (MExpr ([], me, None)) in
+  let mb, (_, cst), _, _ = Mod_typing.translate_module state Subtyping.Cache.empty vm_state env mp0 inl (MExpr ([], me, None)) in
   let sign = mod_type mb in
   let reso = mod_delta mb in
   Modops.subst_modtype_signature_and_resolver mp0 mp sign reso
@@ -202,7 +202,7 @@ let expand_mexpr env mp me =
 let expand_modtype env mp me =
   let inl = Declaremods.default_inline_level () in
   let state = ((Environ.universes env, Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let mtb, _cst, _ = Mod_typing.translate_modtype state vm_state env mp inl ([],me) in
+  let mtb, _cst, _, _ = Mod_typing.translate_modtype state Subtyping.Cache.empty vm_state env mp inl ([],me) in
   mtb
 
 let no_delta = Mod_subst.empty_delta_resolver
diff --git a/test-suite/modules/IncludeSelfChain.v b/test-suite/modules/IncludeSelfChain.v
new file mode 100644
index 000000000000..2691f75a1a8e
--- /dev/null
+++ b/test-suite/modules/IncludeSelfChain.v
@@ -0,0 +1,152 @@
+(* Include-self subtyping checks for chains of functor module types
+   (see rocq-prover/rocq#22279).
+
+   Each [<+] of a functor module type instantiates the functor's parameter
+   with the module type under construction, which triggers a subtyping
+   check of the accumulated signature against the parameter's signature.
+   These tests exercise that path with empty and non-empty parameter
+   signatures, definitions (checked up to conversion), inductive types,
+   submodules, and prefix-shaped chains where the same fields are
+   re-checked at every stage. *)
+
+(* Chains over an empty parameter signature *)
+
+Module Type EmptyArgs. End EmptyArgs.
+Module Type E1 (Import args : EmptyArgs). Parameter e1 : Type. End E1.
+Module Type E2 (Import args : EmptyArgs). Parameter e2 : Type. End E2.
+Module Type E3 (Import args : EmptyArgs). Parameter e3 : Type. End E3.
+
+Module Type EChain := E1 <+ E2 <+ E3.
+
+(* Chains over a shared parameter signature with a couple of fields,
+   including fields referring to each other and a definition *)
+
+Module Type Args.
+  Parameter t : Type.
+  Parameter op : t -> t.
+  Parameter e : t.
+  Definition twice (x : t) : t := op (op x).
+End Args.
+
+Module Type I1 (Import args : Args).
+  Parameter f1 : t -> t.
+End I1.
+Module Type I2 (Import args : Args).
+  Parameter f2 : twice e = twice e.
+End I2.
+
+Module Type Chain := Args <+ I1 <+ I2.
+
+(* The definition [twice] in the accumulated signature is checked, up to
+   conversion, against the definition expected by each parameter. *)
+
+Module Type ArgsEta.
+  Parameter t : Type.
+  Parameter op : t -> t.
+  Parameter e : t.
+  Definition twice : t -> t := fun x => op (op x).
+End ArgsEta.
+
+Module Type I3 (Import args : ArgsEta).
+  Parameter f3 : t.
+End I3.
+
+Module Type ChainEta := Args <+ I3.
+
+(* A parameter cannot implement an expected definition *)
+
+Module Type ArgsDef.
+  Definition d : nat := 0.
+End ArgsDef.
+Module Type UsesDef (Import args : ArgsDef).
+  Parameter u : d = 0.
+End UsesDef.
+
+Module Type BadArgsDef.
+  Parameter d : nat.
+End BadArgsDef.
+
+Fail Module Type BadDefChain := BadArgsDef <+ UsesDef.
+Module Type GoodDefChain := ArgsDef <+ UsesDef.
+
+(* Type mismatches are still detected *)
+
+Module Type BadArgs.
+  Parameter t : Type.
+  Parameter op : t.
+  Parameter e : t.
+  Definition twice (x : t) : t := x.
+End BadArgs.
+
+Fail Module Type BadChain := BadArgs <+ I1.
+
+(* Inductive types and submodules in the parameter signature *)
+
+Module Type ArgsInd.
+  Inductive w : Set := A : w.
+  Module Sub.
+    Definition x : nat := 0.
+  End Sub.
+End ArgsInd.
+
+Module Type I4 (Import args : ArgsInd).
+  Parameter f4 : w -> w.
+End I4.
+
+Module Type ChainInd := ArgsInd <+ I4.
+
+(* Prefix-shaped chains: stage [k] is parameterized by the whole chain up
+   to stage [k-1], so the same fields are re-checked at every stage. *)
+
+Module Type P0. Parameter t0 : Type. End P0.
+Module Type A0 := P0.
+Module Type P1 (Import a : A0). Parameter t1 : Type. End P1.
+Module Type A1 := A0 <+ P1.
+Module Type P2 (Import a : A1). Parameter t2 : Type. End P2.
+Module Type A2 := A1 <+ P2.
+Module Type P3 (Import a : A2). Parameter t3 : Type. End P3.
+Module Type A3 := A2 <+ P3.
+Module Type P4 (Import a : A3). Parameter t4 : Type. End P4.
+Module Type A4 := A3 <+ P4.
+
+(* Functors applied to modules keep checking their argument *)
+
+Module Type Sig.
+  Parameter t : Type.
+  Parameter e : t.
+End Sig.
+
+Module M.
+  Definition t : Type := nat.
+  Definition e : t := 0.
+End M.
+
+Module F (X : Sig).
+  Definition v := X.e.
+End F.
+
+Module App1 := F M.
+Module App2 := F M.
+Module App3 := F M.
+
+Module BadM.
+  Definition t : Type := nat.
+  Definition e : bool := true.
+End BadM.
+
+Fail Module BadApp := F BadM.
+
+(* Includes of applied functors whose argument is a functor parameter *)
+
+Module G (X : Args).
+  Include I1 X.
+End G.
+
+(* Rolling back and redoing a check must reproduce its universe
+   constraints (cached subtyping verdicts are rolled back with the
+   state they were computed in) *)
+
+Set Warnings "-undo-batch-mode".
+Module App4 := F M.
+Reset App4.
+Module App4 := F M.
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 31780b8f57a4..53e186af00f9 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -817,6 +817,13 @@ let vm_state =
   let vm_handler _ _ _ () = (), Vmemitcodes.BCuncompiled in
   ((), { Mod_typing.vm_handler })
 
+(* Cache of the module subtyping field checks performed on the
+   inference side. Cached verdicts stay valid as long as the global
+   environment evolves monotonically; keeping the cache in the summary
+   makes rolling the state back in time also roll the cache back (see
+   {!Subtyping.Cache}). *)
+let subtyping_cache = Summary.ref ~name:"module-subtyping-cache" Subtyping.Cache.empty
+
 module RawModOps = struct
 
 module Synterp = struct
@@ -961,7 +968,8 @@ module Interp = struct
 let check_sub env mp sub_mtb_l =
   let fold sub_mtb (cst, env) =
     let state = ((Environ.universes env, cst), Reductionops.inferred_universes) in
-    let ugraph, cst = Subtyping.check_subtypes state env mp mp sub_mtb in
+    let (ugraph, cst), cache = Subtyping.check_subtypes ~direct:true ~cache:!subtyping_cache state env mp mp sub_mtb in
+    let () = subtyping_cache := cache in
     (cst, Environ.set_universes ugraph env)
   in
   let cst, _ = List.fold_right fold sub_mtb_l (Univ.UnivConstraints.empty, env) in
@@ -1001,7 +1009,8 @@ let build_subtypes env mp args mtys =
       let state = ((Environ.universes env, Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
       (* functor arguments are already part of the env, we compute the type
          and requantify over them *)
-      let mtb, (_, cst), () = Mod_typing.translate_modtype state vm_state env mp inl ([], mte) in
+      let mtb, (_, cst), (), cache = Mod_typing.translate_modtype state !subtyping_cache vm_state env mp inl ([], mte) in
+      let () = subtyping_cache := cache in
       let fold (mbid, mtb, _, _) accu =
         MoreFunctor (mbid, mtb, accu)
       in
@@ -1028,7 +1037,8 @@ let intern_arg (acc, cst) (mbidl,(mty, base, kind, inl)) =
   let () = Global.push_context_set cst' in
   let () =
     let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-    let _, (_, cst), _ = Mod_typing.translate_modtype state vm_state (Global.env ()) base inl ([], mty) in
+    let _, (_, cst), _, cache = Mod_typing.translate_modtype state !subtyping_cache vm_state (Global.env ()) base inl ([], mty) in
+    let () = subtyping_cache := cache in
     Global.add_univ_constraints cst
   in
   let env = Global.env () in
@@ -1074,7 +1084,8 @@ let start_module_core id args res =
         let env = Environ.push_context_set ctx env in
         (* We check immediately that mte is well-formed *)
         let state = ((Environ.universes env, Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-        let _, (_, cst), _ = Mod_typing.translate_modtype state vm_state env mp inl ([], mte) in
+        let _, (_, cst), _, cache = Mod_typing.translate_modtype state !subtyping_cache vm_state env mp inl ([], mte) in
+        let () = subtyping_cache := cache in
         let ctx = Univ.ContextSet.add_constraints cst ctx in
         Some (mte, inl), [], ctx
     | Check resl ->
@@ -1104,10 +1115,11 @@ let end_module_core id m_info objects fs =
   let struc = current_struct () in
   let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) m_info.cur_typ in
   let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let _, (_, cst), _ =
-    Mod_typing.finalize_module state vm_state (Global.env ()) (Global.current_modpath ())
+  let _, (_, cst), _, cache =
+    Mod_typing.finalize_module state !subtyping_cache vm_state (Global.env ()) (Global.current_modpath ())
       (struc, current_modresolver ()) restype'
   in
+  let () = subtyping_cache := cache in
   let () = Global.add_univ_constraints cst in
 
   let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in
@@ -1184,7 +1196,8 @@ let declare_module id args res mexpr_o =
   in
   let () = Global.push_context_set ctx in
   let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let _, (_, cst), _ = Mod_typing.translate_module state vm_state (Global.env ()) mp inl entry in
+  let _, (_, cst), _, cache = Mod_typing.translate_module state !subtyping_cache vm_state (Global.env ()) mp inl entry in
+  let () = subtyping_cache := cache in
   let () = Global.add_univ_constraints cst in
   let mp_env,resolver = Global.add_module id entry inl in
 
@@ -1308,7 +1321,8 @@ let declare_modtype id args mtys (mte,base,kind,inl) =
   let env = Global.env () in
   (* We check immediately that mte is well-formed *)
   let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let _, (_, mte_cst), _ = Mod_typing.translate_modtype state vm_state env mp inl ([], mte) in
+  let _, (_, mte_cst), _, cache = Mod_typing.translate_modtype state !subtyping_cache vm_state env mp inl ([], mte) in
+  let () = subtyping_cache := cache in
   let () = Global.push_context_set (Univ.Level.Set.empty, mte_cst) in
   let params = List.map (fun (mbid, _, mte, b) -> (mbid, mte, b)) params in
   let entry = params, mte in
@@ -1428,9 +1442,10 @@ let declare_one_include_core (me,base,kind,inl) =
   let base_mp = get_module_path me in
 
   let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
-  let sign, (), resolver, (_, cst), _ =
-    Mod_typing.translate_mse_include is_mod state vm_state (Global.env ()) (Global.current_modpath ()) inl me
+  let sign, (), resolver, (_, cst), _, cache =
+    Mod_typing.translate_mse_include is_mod state !subtyping_cache vm_state (Global.env ()) (Global.current_modpath ()) inl me
   in
+  let () = subtyping_cache := cache in
   let () = Global.add_univ_constraints cst in
   let () = assert (ModPath.equal cur_mp (Global.current_modpath ())) in
   (* Include Self support  *)
@@ -1441,7 +1456,8 @@ let declare_one_include_core (me,base,kind,inl) =
       let state = ((Global.universes (), Univ.UnivConstraints.empty), Reductionops.inferred_universes) in
       (* Module subcomponents are already part of env at this point *)
       let env = Environ.shallow_add_module cur_mp mb (Global.env ()) in
-      let (_, cst) = Subtyping.check_subtypes state env cur_mp (MPbound mbid) mtb in
+      let (_, cst), cache = Subtyping.check_subtypes ~direct:true ~cache:!subtyping_cache state env cur_mp (MPbound mbid) mtb in
+      let () = subtyping_cache := cache in
       let () = Global.add_univ_constraints cst in
       let mpsup_delta = match mod_global_delta mb with
       | None -> assert false (* mb is guaranteed not to be a functor here *)