From 1311a2bf08ac1deb16f0b3064bc1164d75858a97 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Jun 2018 14:16:49 +0200 Subject: Remove hack skipping comparison of algebraic universes in subtyping. When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). --- checker/subtyping.ml | 83 ++----------------------------------------- kernel/modops.ml | 1 - kernel/modops.mli | 1 - kernel/subtyping.ml | 81 ++--------------------------------------- kernel/univ.ml | 2 +- test-suite/bugs/closed/7695.v | 20 +++++++++++ vernac/himsg.ml | 3 -- 7 files changed, 25 insertions(+), 166 deletions(-) create mode 100644 test-suite/bugs/closed/7695.v diff --git a/checker/subtyping.ml b/checker/subtyping.ml index f4ae02084..9e9e94deb 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -9,7 +9,6 @@ (************************************************************************) (*i*) -open CErrors open Util open Names open Cic @@ -132,40 +131,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (eq_constr) (fun x -> x.proj_type); true in - let check_inductive_type t1 t2 = - - (* Due to template polymorphism, the conclusions of - t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. - - By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U - |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each - universe in the conclusion of t1 has an bounding universe in - the conclusion of t2, so that we don't need to check the - subtyping of the conclusions of t1 and t2. - - Even if we'd like to recheck it, the inference of constraints - is not designed to deal with algebraic constraints of the form - max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy - to recheck it (in short, we would need the actual graph of - constraints as input while type checking is currently designed - to output a set of constraints instead) *) - - (* So we cheat and replace the subtyping problem on algebraic - constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) - (that we know are necessary true) by trivial constraints that - the constraint generator knows how to deal with *) - - let (ctx1,s1) = dest_arity env t1 in - let (ctx2,s2) = dest_arity env t2 in - let s1,s2 = - match s1, s2 with - | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null - | (Prop _, Type _) | (Type _,Prop _) -> error () - | _ -> (s1, s2) in - check_conv conv_leq env - (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) - in + let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in let check_packet p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -251,52 +217,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (Univ.is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (Univ.is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - error () - with UserError _ (* "not an arity" *) -> - error () end - | _ -> t1,t2 - else - (t1,t2) in - check_conv conv_leq env t1 t2 - in + let check_type env t1 t2 = check_conv conv_leq env t1 t2 in match info1 with | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in diff --git a/kernel/modops.ml b/kernel/modops.ml index 22f523a9a..02bab581a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,7 +47,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/modops.mli b/kernel/modops.mli index ac76d28cf..8e7e618fc 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -106,7 +106,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8cf588c3e..2e9a33a91 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -17,7 +17,6 @@ open Names open Univ open Util -open Term open Constr open Declarations open Declareops @@ -138,39 +137,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = - - (* Due to template polymorphism, the conclusions of - t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. - - By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U - |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each - universe in the conclusion of t1 has an bounding universe in - the conclusion of t2, so that we don't need to check the - subtyping of the conclusions of t1 and t2. - - Even if we'd like to recheck it, the inference of constraints - is not designed to deal with algebraic constraints of the form - max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy - to recheck it (in short, we would need the actual graph of - constraints as input while type checking is currently designed - to output a set of constraints instead) *) - - (* So we cheat and replace the subtyping problem on algebraic - constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) - (that we know are necessary true) by trivial constraints that - the constraint generator knows how to deal with *) - - let (ctx1,s1) = dest_arity env t1 in - let (ctx2,s2) = dest_arity env t2 in - let s1,s2 = - match s1, s2 with - | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop - | (Prop _, Type _) | (Type _,Prop _) -> - error (NotConvertibleInductiveField name) - | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 in let check_packet cst p1 p2 = @@ -259,53 +227,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = - let err = NotConvertibleTypeField (env, t1, t2) in - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - error NoTypeConstraintExpected - with NotArity -> - error err end - | _ -> - t1,t2 - else - (t1,t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly infer_conv_leq env t1 t2 in match info1 with | Constant cb1 -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 2b4a1c50c..311477dac 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -666,7 +666,7 @@ let constraint_add_leq v u c = else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v new file mode 100644 index 000000000..42bdb076b --- /dev/null +++ b/test-suite/bugs/closed/7695.v @@ -0,0 +1,20 @@ +Require Import Hurkens. + +Universes i j k. +Module Type T. + Parameter T1 : Type@{i+1}. + Parameter e : Type@{j} = T1 : Type@{k}. +End T. + +Module M. + Definition T1 := Type@{j}. + Definition e : Type@{j} = T1 : Type@{k} := eq_refl. +End M. + +Module F (A:T). + Definition bad := TypeNeqSmallType.paradox _ A.e. +End F. + +Set Printing Universes. +Fail Module X := F M. +(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5d671ef52..534e58f9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -871,9 +871,6 @@ let explain_not_match_error = function pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" | CumulativeStatusExpected b -> let status b = if b then str"cumulative" else str"non-cumulative" in str "a " ++ status b ++ str" declaration was expected, but a " ++ -- cgit v1.2.3