diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | checker/cic.mli | 2 | ||||
| -rw-r--r-- | checker/declarations.ml | 9 | ||||
| -rw-r--r-- | checker/values.ml | 4 | ||||
| -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 |
8 files changed, 39 insertions, 12 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/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. |