diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 11 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7615.v | 19 |
5 files changed, 29 insertions, 7 deletions
@@ -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/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. |