From e398b8b5dadb0cd75cd6cfb86525ccb039d75d49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 May 2018 01:00:23 +0200 Subject: Fix #7615: Functor inlining drops universe substitution. We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case. --- CHANGES | 1 + kernel/mod_subst.ml | 11 ++++++----- kernel/mod_subst.mli | 2 +- kernel/modops.ml | 3 ++- test-suite/bugs/closed/7615.v | 19 +++++++++++++++++++ 5 files changed, 29 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/7615.v 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/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. -- cgit v1.2.3 From 45e1e0dcba3101b6a9e096f18c28da899615af7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 May 2018 08:40:25 +0200 Subject: Fix the checker by merely adapting the data structure. Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though. --- checker/cic.mli | 2 +- checker/declarations.ml | 9 +++++++-- checker/values.ml | 4 ++-- 3 files changed, 10 insertions(+), 5 deletions(-) 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" -- cgit v1.2.3