diff options
| -rw-r--r-- | kernel/subtyping.ml | 49 | ||||
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | kernel/univ.mli | 1 | ||||
| -rw-r--r-- | test-suite/modules/subtyping.v | 9 |
4 files changed, 62 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index eb7f26cf4..537c20aef 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -195,13 +195,60 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let check_constant cst env msid1 l info1 cb2 spec2 = let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in + let check_type cst 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 Sign.isArity t2 then + let (ctx2,s2) = Sign.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 *) + Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_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 *) + Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_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 () + with UserError _ (* "not an arity" *) -> + error () end + | _ -> t1,t2 + else + (t1,t2) in + check_conv cst conv_leq env t1 t2 + in + match info1 with | Constant cb1 -> assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; (*Start by checking types*) let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = check_conv cst conv_leq env typ1 typ2 in + let cst = check_type cst env typ1 typ2 in let con = make_con (MPself msid1) empty_dirpath l in let cst = match cb2.const_body with diff --git a/kernel/univ.ml b/kernel/univ.ml index a58424d3d..17bd10fc9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -134,6 +134,10 @@ let is_base_univ = function | Max ([Base],[]) -> warning "Non canonical Set"; true | u -> false +let is_univ_variable = function + | Atom a when a<>Base -> true + | _ -> false + (* When typing [Prop] and [Set], there is no constraint on the level, hence the definition of [prop_univ], the type of [Prop] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index a7d27f47c..518c4a62b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -18,6 +18,7 @@ val neutral_univ : universe val make_univ : Names.dir_path * int -> universe val is_base_univ : universe -> bool +val is_univ_variable : universe -> bool (* The type of a universe *) val super : universe -> universe diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v index fb3eae3af..2df8e84e5 100644 --- a/test-suite/modules/subtyping.v +++ b/test-suite/modules/subtyping.v @@ -35,3 +35,12 @@ End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *) (* Note: Top.6 <= Top.1 is generated by subtyping on A; subtyping of L follows and has not to be checked *) + + + +(* The same bug as #1302 but for Definition *) +(* Check that inferred algebraic universes in interfaces are considered *) + +Module Type U. Definition A := Type -> Type. End U. +Module M:U. Definition A := Type -> Type. End M. + |