aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/modops.ml5
-rw-r--r--kernel/modops.mli5
-rw-r--r--kernel/subtyping.ml78
-rw-r--r--kernel/univ.ml6
-rw-r--r--kernel/univ.mli5
-rw-r--r--test-suite/bugs/closed/3670.v23
-rw-r--r--toplevel/himsg.ml17
7 files changed, 122 insertions, 17 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4c18ed275..859f83e05 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -35,6 +35,7 @@ type signature_mismatch_error =
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of env * types * types
+ | PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
@@ -44,6 +45,10 @@ type signature_mismatch_error =
| RecordProjectionsExpected of Name.t list
| NotEqualInductiveAliases
| NoTypeConstraintExpected
+ | IncompatibleInstances
+ | IncompatibleUniverses of Univ.univ_inconsistency
+ | IncompatiblePolymorphism of env * types * types
+ | IncompatibleConstraints of Univ.constraints
type module_typing_error =
| SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a71e28d6e..63d71a566 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -94,6 +94,7 @@ type signature_mismatch_error =
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of env * types * types
+ | PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
@@ -103,6 +104,10 @@ type signature_mismatch_error =
| RecordProjectionsExpected of Name.t list
| NotEqualInductiveAliases
| NoTypeConstraintExpected
+ | IncompatibleInstances
+ | IncompatibleUniverses of Univ.univ_inconsistency
+ | IncompatiblePolymorphism of env * types * types
+ | IncompatibleConstraints of Univ.constraints
type module_typing_error =
| SignatureMismatch of
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f1402a3db..4f54220e7 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -79,8 +79,15 @@ let make_labmap mp list =
List.fold_right add_one list empty_labmap
-let check_conv_error error why cst f env a1 a2 =
- try Constraint.union cst (f env (Environ.universes env) a1 a2)
+let check_conv_error error why cst poly u f env a1 a2 =
+ try
+ let a1 = Vars.subst_instance_constr u a1 in
+ let a2 = Vars.subst_instance_constr u a2 in
+ let cst' = f env (Environ.universes env) a1 a2 in
+ if poly then
+ if Constraint.is_empty cst' then cst
+ else error (IncompatiblePolymorphism (env, a1, a2))
+ else Constraint.union cst cst'
with NotConvertible -> error why
(* for now we do not allow reorderings *)
@@ -89,15 +96,21 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let kn1 = KerName.make2 mp1 l in
let kn2 = KerName.make2 mp2 l in
let error why = error_signature_mismatch l spec2 why in
- let check_conv why cst f = check_conv_error error why cst f in
+ let check_conv why cst poly u f = check_conv_error error why cst poly u f in
let mib1 =
match info1 with
| IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
| _ -> error (InductiveFieldExpected mib2)
in
+ let poly =
+ if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then
+ error (PolymorphicStatusExpected mib2.mind_polymorphic)
+ else mib2.mind_polymorphic
+ in
let u =
- if mib1.mind_polymorphic then
- UContext.instance mib1.mind_universes
+ if poly then
+ Errors.error ("Checking of subtyping of polymorphic" ^
+ " inductive types not implemented")
else Instance.empty
in
let mib2 = Declareops.subst_mind_body subst2 mib2 in
@@ -134,7 +147,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
error (NotConvertibleInductiveField name)
| _ -> (s1, s2) in
check_conv (NotConvertibleInductiveField name)
- cst infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+ cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
in
let check_packet cst p1 p2 =
@@ -161,7 +174,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let mind = mind_of_kn kn1 in
let check_cons_types i cst p1 p2 =
Array.fold_left3
- (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst infer_conv env t1 t2)
+ (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
+ poly u infer_conv env t1 t2)
cst
p2.mind_consnames
(arities_of_specif (mind,u) (mib1,p1))
@@ -221,8 +235,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
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 f = check_conv_error error cst f in
- let check_type cst env t1 t2 =
+ let check_conv cst poly u f = check_conv_error error cst poly u f in
+ let check_type poly u cst env t1 t2 =
let err = NotConvertibleTypeField (env, t1, t2) in
@@ -269,17 +283,47 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
t1,t2
else
(t1,t2) in
- check_conv err cst infer_conv_leq env t1 t2
+ check_conv err cst poly u infer_conv_leq env t1 t2
in
match info1 with
| Constant cb1 ->
let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
let cb1 = Declareops.subst_const_body subst1 cb1 in
let cb2 = Declareops.subst_const_body subst2 cb2 in
- (* 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_type cst env typ1 typ2 in
+ (* Start by checking universes *)
+ let poly =
+ if not (cb1.const_polymorphic == cb2.const_polymorphic) then
+ error (PolymorphicStatusExpected cb2.const_polymorphic)
+ else cb2.const_polymorphic
+ in
+ let cst', env', u =
+ if poly then
+ let ctx1 = Univ.instantiate_univ_context cb1.const_universes in
+ let ctx2 = Univ.instantiate_univ_context cb2.const_universes in
+ let inst1, ctx1 = Univ.UContext.dest ctx1 in
+ let inst2, ctx2 = Univ.UContext.dest ctx2 in
+ if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
+ error IncompatibleInstances
+ else
+ let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
+ let cstrs = Univ.Constraint.union cstrs ctx2 in
+ try
+ (* The environment with the expected universes plus equality
+ of the body instances with the expected instance *)
+ let env = Environ.add_constraints cstrs env in
+ (* Check that the given definition does not add any constraint over
+ the expected ones, so that it can be used in place of the original. *)
+ if Univ.check_constraints ctx1 (Environ.universes env) then
+ cstrs, env, inst2
+ else error (IncompatibleConstraints ctx1)
+ with Univ.UniverseInconsistency incon ->
+ error (IncompatibleUniverses incon)
+ else cst, env, Univ.Instance.empty
+ in
+ (* Now check 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_type poly u cst env' typ1 typ2 in
(* Now we check the bodies:
- A transparent constant can only be implemented by a compatible
transparent constant.
@@ -296,7 +340,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
Anyway [check_conv] will handle that afterwards. *)
let c1 = Mod_subst.force_constr lc1 in
let c2 = Mod_subst.force_constr lc2 in
- check_conv NotConvertibleBodyField cst infer_conv env c1 c2))
+ check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
| IndType ((kn,i),mind1) ->
ignore (Errors.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -312,7 +356,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
let cst = Constraint.union cst (Constraint.union cst1 cst2) in
let error = NotConvertibleTypeField (env, arity1, typ2) in
- check_conv error cst infer_conv_leq env arity1 typ2
+ check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2
| IndConstr (((kn,i),j) as cstr,mind1) ->
ignore (Errors.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -327,7 +371,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
let cst = Constraint.union cst (Constraint.union cst1 cst2) in
let error = NotConvertibleTypeField (env, ty1, ty2) in
- check_conv error cst infer_conv env ty1 ty2
+ check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2
let rec check_modules cst env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module msb1 in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fed053d65..d66ae911d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1717,6 +1717,8 @@ module Instance : sig
val append : t -> t -> t
val equal : t -> t -> bool
+ val length : t -> int
+
val hcons : t -> t
val hash : t -> int
@@ -1792,6 +1794,8 @@ struct
let to_array a = a
+ let length a = Array.length a
+
let subst_fn fn t =
let t' = CArray.smartmap fn t in
if t' == t then t else t'
@@ -1855,6 +1859,8 @@ struct
let union (univs, cst) (univs', cst') =
Instance.append univs univs', Constraint.union cst cst'
+
+ let dest x = x
end
type universe_context = UContext.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7c0c9536f..296868836 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -273,6 +273,9 @@ sig
val equal : t -> t -> bool
(** Equality *)
+ val length : t -> int
+ (** Instance length *)
+
val hcons : t -> t
(** Hash-consing. *)
@@ -318,6 +321,8 @@ sig
val instance : t -> Instance.t
val constraints : t -> constraints
+ val dest : t -> Instance.t * constraints
+
(** Keeps the order of the instances *)
val union : t -> t -> t
diff --git a/test-suite/bugs/closed/3670.v b/test-suite/bugs/closed/3670.v
new file mode 100644
index 000000000..c0f03261a
--- /dev/null
+++ b/test-suite/bugs/closed/3670.v
@@ -0,0 +1,23 @@
+Set Universe Polymorphism.
+Module Type FOO.
+ Parameter f : Type -> Type.
+ Parameter h : forall T, f T.
+End FOO.
+
+Module Type BAR.
+ Include FOO.
+End BAR.
+
+Module Type BAZ.
+ Include FOO.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) <: BAR.
+
+ Definition f : Type -> Type.
+ Proof. exact baz.f. Defined.
+
+ Definition h : forall T, f T.
+ Admitted.
+
+Fail End BAR_FROM_BAZ.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 54f717950..15d6e29eb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -819,6 +819,23 @@ let explain_not_match_error = function
| NoTypeConstraintExpected ->
strbrk "a definition whose type is constrained can only be subtype " ++
strbrk "of a definition whose type is itself constrained"
+ | PolymorphicStatusExpected b ->
+ let status b = if b then str"polymorphic" else str"monomorphic" in
+ str "a " ++ status b ++ str" declaration was expected, but a " ++
+ status (not b) ++ str" declaration was found"
+ | IncompatibleInstances ->
+ str"polymorphic universe instances do not match"
+ | IncompatibleUniverses incon ->
+ str"the universe constraints are inconsistent: " ++
+ Univ.explain_universe_inconsistency incon
+ | IncompatiblePolymorphism (env, t1, t2) ->
+ str "conversion of polymorphic values generates additional constraints: " ++
+ quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
+ str "compared to " ++ spc () ++
+ quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
+ | IncompatibleConstraints cst ->
+ str " the expected (polymorphic) constraints do not imply " ++
+ quote (Univ.pr_constraints cst)
let explain_signature_mismatch l spec why =
str "Signature components for label " ++ str (Label.to_string l) ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 14:37:48 +0000