Merge PR #8974: Fix mod_subst wrt universe polymorphism

19 files changed, 120 insertions, 77 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 863f965896..1afe764ca4 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -168,8 +168,10 @@ let v_section_ctxt = v_enum "emptylist" 1
 
 (** kernel/mod_subst *)
 
+let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
+
 let v_delta_hint =
-  v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
+  v_sum "delta_hint" 0 [|[|Int; Opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
 
 let v_resolver =
   v_tuple "delta_resolver"
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 55a87fcd4d..8d225fe683 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw =
   match raw with
   | NRef ref ->
       let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-	  fst (notation_constr_of_constr bound t)
+      if ref' == ref then raw else (match t with
+          | None -> NRef ref'
+          | Some t ->
+            fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
 
   | NVar _ -> raw
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8e5d15dd2d..d67d15b23b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1361,7 +1361,7 @@ type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
 
-(* Sorts and sort family *)
+(** Minimalistic constr printer, typically for debugging *)
 
 let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
   let open Pp in
@@ -1377,8 +1377,6 @@ let pr_puniverses p u =
   if Univ.Instance.is_empty u then p
   else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
 
-(* Minimalistic constr printer, typically for debugging *)
-
 let rec debug_print c =
   let open Pp in
   match kind c with
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 2a91c7dab0..52fb39e1d0 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 * (Univ.AUContext.t * constr) option
+  | Inline of int * constr Univ.univ_abstracted option
   | Equiv of KerName.t
 
 (* NB: earlier constructor Prefix_equiv of ModPath.t
@@ -164,7 +164,7 @@ let find_prefix resolve mp =
 
 (** Applying a resolver to a kernel name *)
 
-exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr))
+exception Change_equiv_to_inline of (int * constr Univ.univ_abstracted)
 
 let solve_delta_kn resolve kn =
   try
@@ -294,43 +294,34 @@ let subst_ind sub (ind,i as indi) =
 let subst_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
-let subst_con0 sub (cst,u) =
+let subst_con0 sub cst =
   let mpu,l = Constant.repr2 cst in
   let mpc = KerName.modpath (Constant.canonical cst) in
   let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
   let knu = KerName.make mpu l in
   let knc = if mpu == mpc then knu else KerName.make mpc l in
   match search_delta_inline resolve knu knc with
-    | Some (ctx, t) ->
+    | Some t ->
       (* In case of inlining, discard the canonical part (cf #2608) *)
-      let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in
-      Constant.make1 knu, Vars.subst_instance_constr u t
+      Constant.make1 knu, Some t
     | None ->
       let knc' =
         progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
       in
       let cst' = Constant.make knu knc' in
-      cst', mkConstU (cst',u)
+      cst', None
 
 let subst_con sub cst =
   try subst_con0 sub cst
-  with No_subst -> fst cst, mkConstU cst
+  with No_subst -> cst, None
 
-let subst_con_kn sub con =
-  subst_con sub (con,Univ.Instance.empty)
-
-let subst_pcon sub (_con,u as pcon) =
-  try let con', _can = subst_con0 sub pcon in
+let subst_pcon sub (con,u as pcon) =
+  try let con', _can = subst_con0 sub con in
 	con',u
   with No_subst -> pcon
 
-let subst_pcon_term sub (_con,u as pcon) =
-  try let con', can = subst_con0 sub pcon in 
-	(con',u), can
-  with No_subst -> pcon, mkConstU pcon
-
 let subst_constant sub con =
-  try fst (subst_con0 sub (con,Univ.Instance.empty))
+  try fst (subst_con0 sub con)
   with No_subst -> con
 
 let subst_proj_repr sub p =
@@ -351,7 +342,7 @@ let subst_evaluable_reference subst = function
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind c with
-      | Const kn -> (try snd (f' kn) with No_subst -> c)
+      | Const kn -> (try f' kn with No_subst -> c)
       | Proj (p,t) -> 
           let p' = Projection.map f p in
 	  let t' = func t in
@@ -420,8 +411,14 @@ let rec map_kn f f' c =
       | _ -> c
 
 let subst_mps sub c =
+  let subst_pcon_term sub (con,u) =
+    let con', can = subst_con0 sub con in
+    match can with
+    | None -> mkConstU (con',u)
+    | Some t -> Vars.univ_instantiate_constr u t
+  in
   if is_empty_subst sub then c
-  else map_kn (subst_mind sub) (subst_con0 sub) c
+  else map_kn (subst_mind sub) (subst_pcon_term sub) c
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
@@ -486,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 (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
+      | Inline (lev,Some t) -> Inline (lev,Some (Univ.map_univ_abstracted (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 8416094063..ea391b3de7 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 * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
+  KerName.t -> (int * constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
@@ -133,17 +133,11 @@ val subst_kn :
   substitution -> KerName.t -> KerName.t
 
 val subst_con :
-  substitution -> pconstant -> Constant.t * constr
+  substitution -> Constant.t -> Constant.t * constr Univ.univ_abstracted option
 
 val subst_pcon :
   substitution -> pconstant -> pconstant
 
-val subst_pcon_term :
-  substitution -> pconstant -> pconstant * constr
-
-val subst_con_kn :
-  substitution -> Constant.t -> Constant.t * constr
-
 val subst_constant :
   substitution -> Constant.t -> Constant.t
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index f43dbd88f9..97ac3cdebb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	    | Def body ->
 	      let constr = Mod_subst.force_constr body in
               let ctx = Declareops.constant_polymorphic_context constant in
-              add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
+              let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
+              add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (Constant.label con)
 	    (ModPath.to_string (Constant.modpath con))
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7b5ed05bda..93a91af1d7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -978,6 +978,15 @@ struct
 
 end
 
+type 'a univ_abstracted = {
+  univ_abstracted_value : 'a;
+  univ_abstracted_binder : AUContext.t;
+}
+
+let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
+  let univ_abstracted_value = f univ_abstracted_value in
+  {univ_abstracted_value;univ_abstracted_binder}
+
 let hcons_abstract_universe_context = AUContext.hcons
 
 (** Universe info for cumulative inductive types: A context of
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 512f38cedd..8327ff1644 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -360,6 +360,14 @@ sig
 
 end
 
+type 'a univ_abstracted = {
+  univ_abstracted_value : 'a;
+  univ_abstracted_binder : AUContext.t;
+}
+(** A value with bound universe levels. *)
+
+val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
+
 (** Universe info for cumulative inductive types: A context of
    universe levels with universe constraints, representing local
    universe variables and constraints, together with an array of
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f9c576ca4a..bd56d60053 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,6 +295,11 @@ let subst_instance_constr subst c =
     in
     aux c
 
+let univ_instantiate_constr u c =
+  let open Univ in
+  assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
+  subst_instance_constr u c.univ_abstracted_value
+
 (* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
 (* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
 
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 7c928e2694..f2c32b3625 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -140,4 +140,7 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context
 val subst_instance_constr : Instance.t -> constr -> constr
 val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
 
+val univ_instantiate_constr : Instance.t -> constr univ_abstracted -> constr
+(** Ignores the constraints carried by [univ_abstracted]. *)
+
 val universes_of_constr : constr -> Univ.LSet.t
diff --git a/library/globnames.ml b/library/globnames.ml
index 9aca7788d2..db2e8bfaed 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,8 +31,8 @@ let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destCon
 
 let subst_constructor subst (ind,j as ref) =
   let ind' = subst_ind subst ind in
-    if ind==ind' then ref, mkConstruct ref
-    else (ind',j), mkConstruct (ind',j)
+  if ind==ind' then ref
+  else (ind',j)
 
 let subst_global_reference subst ref = match ref with
   | VarRef var -> ref
@@ -43,20 +43,20 @@ let subst_global_reference subst ref = match ref with
     let ind' = subst_ind subst ind in
       if ind==ind' then ref else IndRef ind'
   | ConstructRef ((kn,i),j as c) ->
-    let c',t = subst_constructor subst c in
-      if c'==c then ref else ConstructRef c'
+    let c' = subst_constructor subst c in
+    if c'==c then ref else ConstructRef c'
 
 let subst_global subst ref = match ref with
-  | VarRef var -> ref, mkVar var
+  | VarRef var -> ref, None
   | ConstRef kn ->
-     let kn',t = subst_con_kn subst kn in
-      if kn==kn' then ref, mkConst kn else ConstRef kn', t
+     let kn',t = subst_con subst kn in
+      if kn==kn' then ref, None else ConstRef kn', t
   | IndRef ind ->
       let ind' = subst_ind subst ind in
-      if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind'
+      if ind==ind' then ref, None else IndRef ind', None
   | ConstructRef ((kn,i),j as c) ->
-      let c',t = subst_constructor subst c in
-	if c'==c then ref,t else ConstructRef c', t
+      let c' = subst_constructor subst c in
+      if c'==c then ref,None else ConstructRef c', None
 
 let canonical_gr = function
   | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
diff --git a/library/globnames.mli b/library/globnames.mli
index a96a42ced2..d49ed453f5 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -36,8 +36,8 @@ val destConstructRef : GlobRef.t -> constructor
 
 val is_global : GlobRef.t -> constr -> bool
 
-val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_constructor : substitution -> constructor -> constructor
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
 (** This constr is not safe to be typechecked, universe polymorphism is not 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f18040accb..306a76e35e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,9 +192,11 @@ let subst_cl_typ subst ct = match ct with
     let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
-      let c',t = subst_con_kn subst c in
-	if c' == c then ct else
-         pi1 (find_class_type Evd.empty (EConstr.of_constr t))
+      let c',t = subst_con subst c in
+      if c' == c then ct else (match t with
+          | None -> CL_CONST c'
+          | Some t ->
+            pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
   | CL_IND i ->
       let i' = subst_ind subst i in
 	if i' == i then ct else CL_IND i'
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 09b3cf167f..517834f014 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -948,10 +948,13 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
     let ref',t = subst_global subst ref in
-    if ref' == ref then raw else
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
+    if ref' == ref then raw else (match t with
+        | None -> GRef (ref', u)
+        | Some t ->
+          let env = Global.env () in
+          let evd = Evd.from_env env in
+          let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *)
+          DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)))
 
   | GSort _
   | GVar _
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index e533930267..ccbb2934bc 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -147,13 +147,16 @@ let cache_head o =
 
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con_kn subst cst in
-      if isConst c && Constant.equal (fst (destConst c)) cst then
-        (* A change of the prefix of the constant *)
-        k
-      else
-        (* A substitution of the constant by a functor argument *)
-        kind_of_head (Global.env()) c
+    let cst',c = subst_con subst cst in
+    if cst == cst' then k
+    else
+      (match c with
+       | None ->
+         (* A change of the prefix of the constant *)
+         RigidHead (RigidParameter cst')
+       | Some c ->
+         (* A substitution of the constant by a functor argument *)
+         kind_of_head (Global.env()) c.Univ.univ_abstracted_value)
   | x -> x
 
 let subst_head (subst,(ref,k)) =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a3ab250784..248d5d0a0e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,10 +279,12 @@ let rec subst_pattern subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
-    if ref' == ref then pat else
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      pattern_of_constr env evd t
+    if ref' == ref then pat else (match t with
+        | None -> PRef ref'
+        | Some t ->
+          let env = Global.env () in
+          let evd = Evd.from_env env in
+          pattern_of_constr env evd t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 0c4a2e2a99..6e3b19ae61 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -71,12 +71,12 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    List.Smart.map
-     (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
+     (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = fst (subst_constructor subst id) in
-    if projs' == projs && kn' == kn && id' == id then obj else
-      ((kn',i),id',kl,projs')
+  let id' = subst_constructor subst id in
+  if projs' == projs && kn' == kn && id' == id then obj else
+    ((kn',i),id',kl,projs')
 
 let discharge_structure (_,x) = Some x
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c20feccace..faff116af4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1063,12 +1063,12 @@ let cache_autohint (kn, obj) =
 
 let subst_autohint (subst, obj) =
   let subst_key gr =
-    let (lab'', elab') = subst_global subst gr in
-    let elab' = EConstr.of_constr elab' in
-    let gr' =
-      (try head_constr_bound Evd.empty elab'
-       with Bound -> lab'')
-    in if gr' == gr then gr else gr'
+    let (gr', t) = subst_global subst gr in
+    match t with
+    | None -> gr'
+    | Some t ->
+      (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+       with Bound -> gr')
   in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
diff --git a/test-suite/bugs/closed/bug_8951.v b/test-suite/bugs/closed/bug_8951.v
new file mode 100644
index 0000000000..dce19318c5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8951.v
@@ -0,0 +1,14 @@
+Module Type T.
+  Polymorphic Parameter Inline t@{i} : Type@{i}.
+End T.
+
+Module M.
+  Polymorphic Definition t@{i} := nat.
+End M.
+
+Module Make (X:T).
+  Include X.
+
+End Make.
+
+Module P := Make M.