Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.

8 files changed, 39 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index 787c9ba12..ce8e313b9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,7 @@ Changes from 8.8.0 to 8.8.1
 Kernel
 
 - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with inlining of polymorphic constants (#7615).
 
 Notations
 
diff --git a/checker/cic.mli b/checker/cic.mli
index 27e2a479f..7ec345768 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,7 +128,7 @@ type section_context = unit
 (** {6 Substitutions} *)
 
 type delta_hint =
-  | Inline of int * constr option
+  | Inline of int * (Univ.AUContext.t * constr) option
   | Equiv of KerName.t
 
 type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
diff --git a/checker/declarations.ml b/checker/declarations.ml
index e1d2cf6d1..a744a0227 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -196,7 +196,12 @@ let subst_con0 sub con u =
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
-    | Some t -> con', t
+    | Some (ctx, t) ->
+      (** FIXME: we never typecheck the inlined term, so that it could well
+          be garbage. What environment do we type it in though? The substitution
+          code should be moot in the checker but it **is** used nonetheless. *)
+      let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in
+      con', subst_instance_constr u t
     | None ->
       let con'' = match side with
 	| User -> constant_of_delta resolve con'
@@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver =
     let kkey' = if dom then subst_kn subst kkey else kkey in
     let hint' = match hint with
       | Equiv kequ -> Equiv (subst_kn_delta subst kequ)
-      | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+      | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
       | Inline (_,None) -> hint
     in
     Deltamap.add_kn kkey' hint' rslv
diff --git a/checker/values.ml b/checker/values.ml
index f7ab95fe2..67032bd1b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
+MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
 
 *)
 
@@ -173,7 +173,7 @@ let v_section_ctxt = v_enum "emptylist" 1
 (** kernel/mod_subst *)
 
 let v_delta_hint =
-  v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|]
+  v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
 
 let v_resolver =
   v_tuple "delta_resolver"
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 0027ebecf..a47af56ca 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -24,7 +24,7 @@ open Constr
    is the term into which we should inline. *)
 
 type delta_hint =
-  | Inline of int * constr option
+  | Inline of int * (Univ.AUContext.t * constr) option
   | Equiv of KerName.t
 
 (* NB: earlier constructor Prefix_equiv of ModPath.t
@@ -158,7 +158,7 @@ let find_prefix resolve mp =
 
 (** Applying a resolver to a kernel name *)
 
-exception Change_equiv_to_inline of (int * constr)
+exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr))
 
 let solve_delta_kn resolve kn =
   try
@@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) =
   let knu = KerName.make mpu dir l in
   let knc = if mpu == mpc then knu else KerName.make mpc dir l in
   match search_delta_inline resolve knu knc with
-    | Some t ->
+    | Some (ctx, t) ->
       (* In case of inlining, discard the canonical part (cf #2608) *)
-      Constant.make1 knu, t
+      let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in
+      Constant.make1 knu, Vars.subst_instance_constr u t
     | None ->
       let knc' =
         progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
@@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver =
       | Equiv kequ ->
 	  (try Equiv (subst_kn_delta subst kequ)
 	   with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
-      | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+      | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
       | Inline (_,None) -> hint
     in
     Deltamap.add_kn kkey' hint' rslv
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index b14d39207..76a1d173b 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
   KerName.t -> KerName.t -> delta_resolver -> delta_resolver
 
 val add_inline_delta_resolver :
-  KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
+  KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 203817118..22f523a9a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
 	      let constr = Mod_subst.force_constr body in
-	      add_inline_delta_resolver kn (lev, Some constr) l
+              let ctx = Declareops.constant_polymorphic_context constant in
+              add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
 	with Not_found ->
 	  error_no_such_label_sub (Constant.label con)
 	    (ModPath.to_string (Constant.modpath con))
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 000000000..cd8c4ad7d
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.