Merge PR #22451: Correctly implement δ-resolver lift for modules.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

Author: coqbot-app[bot]

checker/values.ml

@@ -300,9 +300,11 @@ let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
 let v_delta_hint =
   v_sum "delta_hint" 0 [|[|v_int; v_opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
 
+let v_mp_hint = v_sum "mp_hint" 1 [|[|v_mp|]|]
+
 let v_resolver =
   v_tuple "delta_resolver"
-    [|v_mp; v_map v_mp v_mp;
+    [|v_mp; v_map v_mp v_mp_hint;
       v_hmap v_kn v_delta_hint|]
 
 let v_subst =

kernel/mod_subst.ml

@@ -20,10 +20,17 @@ open Util
 open Names
 open Constr
 
+(* The modpath part of a resolver holds two kinds of statements.
+   - [p ↦ MPequiv q] states that [q] is the canonical name of [p].
+   - [p ↦ MPlift] states that [p] is a bound name that should be left untouched
+     by substitution. *)
+type mp_hint =
+| MPequiv of ModPath.t  (** the canonical form of the key *)
+| MPlift                (** the prefix rule stops here *)
+
 (* For Inline, the int is an inlining level, and the constr (if present)
    is the term into which we should inline.
    Equiv gives the canonical name in the given context. *)
-
 type delta_hint =
   | Inline of int * constr UVars.univ_abstracted option
   | Equiv of KerName.t
@@ -35,7 +42,7 @@ module Deltamap = struct
   type t = {
     root : ModPath.t;
     (** Common root of all keys in the deltamap *)
-    mmap : ModPath.t ModPath.Map.t;
+    mmap : mp_hint ModPath.Map.t;
     (** All bindings [mp ↦ _] must satisfy [mp ⊆ root] *)
     kmap : delta_hint KerName.Map.t;
     (** All bindings [kn ↦ _] must satisfy [modpath(kn) ⊆ root] *)
@@ -53,16 +60,19 @@ module Deltamap = struct
     let () = assert (ModPath.subpath reso.root (KerName.modpath kn)) in
     { reso with kmap = KerName.Map.add kn hint reso.kmap }
 
-  let add_mp mp mp' reso =
+  let add_mp_hint mp hint reso =
     let () = assert (ModPath.subpath reso.root mp) in
-    { reso with mmap = ModPath.Map.add mp mp' reso.mmap }
+    { reso with mmap = ModPath.Map.add mp hint reso.mmap }
 
-  let find_mp mp reso = ModPath.Map.find mp reso.mmap
+  let add_mp mp mp' reso = add_mp_hint mp (MPequiv mp') reso
+  let lift_mp mp reso = add_mp_hint mp MPlift reso
+
+  let find_mp_opt mp reso = ModPath.Map.find_opt mp reso.mmap
   let find_kn kn reso = KerName.Map.find kn reso.kmap
   let fold_kn f reso i = KerName.Map.fold f reso.kmap i
   let fold fmp fkn reso accu =
     ModPath.Map.fold fmp reso.mmap (KerName.Map.fold fkn reso.kmap accu)
-  let join map1 map2 = fold add_mp add_kn map1 map2
+  let join map1 map2 = fold add_mp_hint add_kn map1 map2
 
   (** if mp0 ⊆ root, we can see a resolver on root as a resolver on mp *)
   let upcast mp0 reso =
@@ -87,8 +97,8 @@ module Deltamap = struct
             path in mm above root, as find_prefix will always return this one
             without considering the less precise ones. *)
           let glb = match glb with
-          | None -> Some mp
-          | Some glb -> if ModPath.subpath glb mp then Some mp else Some glb
+          | None -> Some (mp, data)
+          | Some (g, _) as old -> if ModPath.subpath g mp then Some (mp, data) else old
           in
           glb, accu
         else
@@ -98,21 +108,23 @@ module Deltamap = struct
       let glb, mm' = ModPath.Map.fold fold_mp mm (None, ModPath.Map.empty) in
       let mm' = match glb with
       | None -> mm'
-      | Some glb ->
+      | Some (glb, data) ->
         if ModPath.Map.mem root mm then mm'
         else
           (* Add root to the resolver and map it to what find_prefix would have
             returned on root *)
-          let rec diff accu mp =
-            if ModPath.equal mp glb then accu
-            else match mp with
-            | MPdot (mp, l) -> diff (l :: accu) mp
-            | MPbound _ | MPfile _ -> assert false
-          in
-          let diff = diff [] root in
-          let data = ModPath.Map.get glb mm in
-          let data' = List.fold_left (fun accu l -> MPdot (accu, l)) data diff in
-          ModPath.Map.add root data' mm'
+          match data with
+          | MPlift -> ModPath.Map.add root MPlift mm'
+          | MPequiv data ->
+            let rec diff accu mp =
+              if ModPath.equal mp glb then accu
+              else match mp with
+              | MPdot (mp, l) -> diff (l :: accu) mp
+              | MPbound _ | MPfile _ -> assert false
+            in
+            let diff = diff [] root in
+            let data' = List.fold_left (fun accu l -> MPdot (accu, l)) data diff in
+            ModPath.Map.add root (MPequiv data') mm'
       in
       (* filter the kernames *)
       let filter_kn kn _ = ModPath.subpath root (KerName.modpath kn) in
@@ -166,12 +178,16 @@ let string_of_hint pr = function
   | Inline (lvl, None) -> str "inline[" ++ int lvl ++ str "]"
   | Equiv kn -> str "equiv(" ++ KerName.print kn ++ str ")"
 
+let debug_pr_mp_hint = function
+| MPequiv mp -> ModPath.print mp
+| MPlift -> str "<lift>"
+
 let debug_pr_delta pr resolve =
   let kn_to_string kn hint l =
     hov 2 (KerName.print kn ++ str " =>" ++ spc() ++ string_of_hint pr hint) :: l
   in
-  let mp_to_string mp mp' l =
-    hov 2 (ModPath.print mp ++ str " =>" ++ spc() ++ ModPath.print mp') :: l
+  let mp_to_string mp hint l =
+    hov 2 (ModPath.print mp ++ str " =>" ++ spc() ++ debug_pr_mp_hint hint) :: l
   in
   let l = Deltamap.fold mp_to_string kn_to_string resolve [] in
   v 0 @@ prlist_with_sep pr_comma (fun p -> p) (List.rev l)
@@ -207,7 +223,11 @@ let add_kn_delta_resolver kn kn' =
   assert (Id.equal (KerName.label kn) (KerName.label kn'));
   Deltamap.add_kn kn (Equiv kn')
 
-let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
+let add_mp_delta_resolver mp1 mp2 =
+  let () = assert (not (ModPath.equal mp1 mp2)) in
+  Deltamap.add_mp mp1 mp2
+
+let lift_mp_delta_resolver mp = Deltamap.lift_mp mp
 
 (** Extending a [substitution] without sequential composition *)
 
@@ -223,13 +243,19 @@ let map_mbid mbid mp resolve =
 let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
 
 let find_prefix resolve mp =
-  let rec sub_mp = function
-    | MPdot(mp,l) as mp_sup ->
-        (try Deltamap.find_mp mp_sup resolve
-         with Not_found -> MPdot(sub_mp mp,l))
-    | p -> Deltamap.find_mp p resolve
+  let rec sub_mp mp = match Deltamap.find_mp_opt mp resolve with
+  | Some (MPequiv mp') -> mp'
+  | Some MPlift -> mp
+  | None ->
+    match mp with
+    | MPdot (mp1, l) ->
+      (* Preserving sharing is not an optimisation: [progress] in [subst_con0]
+         and [subst_mind] tests with [!=]. This should be fixed at some point. *)
+      let mp1' = sub_mp mp1 in
+      if mp1' == mp1 then mp else MPdot (mp1', l)
+    | MPbound _ | MPfile _ -> mp
   in
-  try sub_mp mp with Not_found -> mp
+  sub_mp mp
 
 (* TODO: remove the indirection at some point *)
 let mp_of_delta = find_prefix
@@ -543,8 +569,8 @@ let replace_mp_in_kn mpfrom mpto kn =
 let mp_in_mp = ModPath.subpath
 
 let subset_prefixed_by mp resolver =
-  let mp_prefix mkey mequ rslv =
-    if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv
+  let mp_prefix mkey hint rslv =
+    if mp_in_mp mp mkey then Deltamap.add_mp_hint mkey hint rslv else rslv
   in
   let kn_prefix kn hint rslv =
     match hint with
@@ -557,8 +583,8 @@ let subset_prefixed_by mp resolver =
 let subst_dom_delta_resolver mp_from mp_to resolver =
   let () = assert (ModPath.equal mp_from resolver.Deltamap.root) in
   let subst = map_mp mp_from mp_to (empty_delta_resolver mp_to) in
-  let mp_apply_subst mkey mequ rslv =
-    Deltamap.add_mp (subst_mp subst mkey) mequ rslv
+  let mp_apply_subst mkey hint rslv =
+    Deltamap.add_mp_hint (subst_mp subst mkey) hint rslv
   in
   let kn_apply_subst kkey hint rslv =
     Deltamap.add_kn (subst_kn subst kkey) hint rslv
@@ -594,10 +620,13 @@ let subst_mp_delta subst mp mkey =
       reso, mp1
 
 let gen_subst_delta_resolver dom subst resolver =
-  let mp_apply_subst mkey mequ rslv =
+  let mp_apply_subst mkey hint rslv =
     let mkey' = if dom then subst_mp subst mkey else mkey in
-    let rslv',mequ' = subst_mp_delta subst mequ mkey' in
-    Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv)
+    match hint with
+    | MPlift -> Deltamap.add_mp_hint mkey' MPlift rslv
+    | MPequiv mequ ->
+      let rslv', mequ' = subst_mp_delta subst mequ mkey' in
+      Deltamap.join rslv' (Deltamap.add_mp_hint mkey' (MPequiv mequ') rslv)
   in
   let kn_apply_subst kkey hint rslv =
     let kkey' = if dom then subst_kn subst kkey else kkey in
@@ -615,8 +644,10 @@ let subst_codom_delta_resolver = gen_subst_delta_resolver false
 let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true
 
 let update_delta_resolver resolver1 resolver2 =
-  let mp_apply_rslv mkey mequ rslv =
-    Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
+  let mp_apply_rslv mkey hint rslv = match hint with
+    | MPlift -> Deltamap.add_mp_hint mkey MPlift rslv
+    | MPequiv mequ ->
+      Deltamap.add_mp_hint mkey (MPequiv (find_prefix resolver2 mequ)) rslv
   in
   let kn_apply_rslv kkey hint1 rslv =
     let hint = match hint1 with

kernel/mod_subst.mli

@@ -25,10 +25,16 @@ val empty_delta_resolver : ModPath.t -> delta_resolver
 
 val has_root_delta_resolver : ModPath.t -> delta_resolver -> bool
 
-(** [add_mp_delta_resolver mp v reso] assumes that root(reso) ⊆ mp. *)
+(** [add_mp_delta_resolver mp v reso] assumes that root(reso) ⊆ mp and mp ≠ v. *)
 val add_mp_delta_resolver :
   ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver
 
+(** [lift_mp_delta_resolver mp reso] marks [mp] as being a bound name that must
+    be left untouched by substitution. This is the semantics of delayed
+    resolvers for functors and module types. Assumes that root(reso) ⊆ mp. *)
+val lift_mp_delta_resolver :
+  ModPath.t -> delta_resolver -> delta_resolver
+
 (** [add_kn_delta_resolver kn v reso] assumes that root(reso) ⊆ modpath(kn). *)
 val add_kn_delta_resolver :
   KerName.t -> KerName.t -> delta_resolver -> delta_resolver

kernel/modops.ml

@@ -293,7 +293,7 @@ let rec strengthen_module mp mb = match mod_type mb with
   if mp_is_alias delta_mb mp then mb (* already strengthened *)
   else
     let reso, struc' = strengthen_signature mp struc delta_mb in
-    let reso = add_mp_delta_resolver mp mp (add_delta_resolver delta_mb reso) in
+    let reso = lift_mp_delta_resolver mp (add_delta_resolver delta_mb reso) in
     strengthen_module_body ~src:mp (NoFunctor struc') reso mb
 | MoreFunctor _ -> mb
 
@@ -307,7 +307,7 @@ and strengthen_signature mp struc reso0 =
     let reso = match mod_global_delta mb with
     | None ->
       (* See {!strengthen_and_subst_module} *)
-      add_mp_delta_resolver mp' mp' reso
+      lift_mp_delta_resolver mp' reso
     | Some delta ->
       add_delta_resolver delta reso
     in
@@ -324,7 +324,7 @@ let strengthen mtb mp = match mod_type mtb with
   if mp_is_alias delta_mtb mp then mtb
   else
     let reso', struc' = strengthen_signature mp struc delta_mtb in
-    let reso' = add_delta_resolver delta_mtb (add_mp_delta_resolver mp mp reso') in
+    let reso' = add_delta_resolver delta_mtb (lift_mp_delta_resolver mp reso') in
     strengthen_module_type struc' reso' mtb
 | MoreFunctor _ -> mtb
 
@@ -408,7 +408,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso =
            semantic for functor this should be changed.*)
         begin match mod_global_delta mb' with
         | None -> (* functor case *)
-          add_mp_delta_resolver mp_to' mp_to' reso', item'
+          lift_mp_delta_resolver mp_to' reso', item'
         | Some delta ->
           add_delta_resolver delta reso', item'
         end
@@ -418,7 +418,7 @@ and strengthen_and_subst_struct struc subst mp_from mp_to alias incl reso =
         let subst' = add_mp mp_from' mp_to' (empty_delta_resolver mp_to') subst in
         let mty' = subst_modtype subst_dom_codom subst' mp_from' mty in
         let item' = if mty' == mty then item else (l, SFBmodtype mty') in
-        add_mp_delta_resolver mp_to' mp_to' reso', item'
+        lift_mp_delta_resolver mp_to' reso', item'
   in
   List.Smart.fold_left_map strengthen_and_subst_field (empty_delta_resolver mp_to) struc
 
@@ -449,7 +449,7 @@ let expand_self_delta mp sign reso =
     let self = mp_of_delta reso mp in
     (* [mp] is only equivalent to itself, it stops the prefix rule from reaching
        the fields the includer will get later. *)
-    let reso0 = add_mp_delta_resolver mp mp reso in
+    let reso0 = lift_mp_delta_resolver mp reso in
     let expand accu (l, item) = match item with
     | SFBconst _ | SFBmind _ | SFBrules _ ->
       let kn = KerName.make mp l in
@@ -465,7 +465,7 @@ let expand_self_delta mp sign reso =
     | SFBmodtype _ ->
       (* as in [strengthen_and_subst_struct], module types are only equivalent
          to themselves *)
-      add_mp_delta_resolver (MPdot (mp, l)) (MPdot (mp, l)) accu
+      lift_mp_delta_resolver (MPdot (mp, l)) accu
     in
     List.fold_left expand reso0 (struct_of_signature sign)
 

test-suite/modules/resolver_prefix_marker.v

@@ -0,0 +1,69 @@
+(* A delta-resolver binding on a modpath records either the canonical form of
+   that path, or a marker saying that the prefix rule must not be extrapolated
+   into it ([Mod_subst.lift_mp_delta_resolver], recorded by
+   [Modops.strengthen_and_subst_struct] for every functor field and every module
+   type field of the module it builds).
+
+   The two transport differently -- a canonical name is left alone, a marker
+   travels with its key -- and while both were spelled [p -> p] they were
+   indistinguishable, so α-renaming a resolver turned a marker into a genuine
+   alias to the source. The two directions of the equivalence check that
+   [Subtyping.check_signatures] runs on a module type field then disagreed on
+   the canonical name of the inductive declared inside it, and the sealing below
+   was rejected with an error that could not even be printed. *)
+
+Module Type HasS. Module Type S. Inductive I := c. End S. End HasS.
+Module Type T. Declare Module M : HasS. End T.
+
+Module B.
+  Module Type S. Inductive I := c. End S.
+End B.
+
+Module C := B. (* first hop: marks C.S *)
+
+Module D : T.
+  Module M := C. (* second hop: used to lose the mark *)
+End D.
+
+(* The same shape with a functor field rather than a module type field, the
+   other kind of field [strengthen_and_subst_struct] marks. It takes a
+   [with Module] to make the parameter type's [M] be [B'] itself, so that the
+   two sides of the check compare the resolver of [B'] with the ambient one;
+   sealing against a module type that merely declares a functor field of the
+   same shape gives them nothing in common to disagree about. The parameter type
+   of [Fn] must have content, for the same reason.
+
+   On its own this no longer trips anything -- the [subst_mp_delta] fix of
+   #22445 is enough for it -- so it is kept as a guard on the marker of a
+   functor field, not as a reproducer. *)
+
+Module Type Any. End Any.
+Module Type TAny. Declare Module M : Any. End TAny.
+
+Module Type WithI. Inductive I := c. End WithI.
+
+Module B'.
+  Module Fn (X : WithI) := X.
+End B'.
+
+Module D' : TAny with Module M := B'.
+  Module M := B'.
+End D'.
+
+(* Another funky test. *)
+
+Module Other.
+
+Module A.
+  Module E. Definition n := false. End E.
+  Module B.
+    Module P. Include A.E. End P.
+  End B.
+  Include B.
+End A.
+
+Include A.
+
+Definition p := P.n.
+
+End Other.