diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-24 13:09:57 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-24 13:09:57 +0200 |
commit | affdcf6d3b66fd446dda09a9e1652e7558b61eaa (patch) | |
tree | bc5c2e313a8462c29975be24296c2a35ac68a180 | |
parent | 4ce199bf63f8e9d209757ddcc25a63fa565f1546 (diff) | |
parent | 5af5bff88fa49731acbf24d8a67148e4215446bd (diff) |
Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants
-rw-r--r-- | checker/subtyping.ml | 13 | ||||
-rw-r--r-- | test-suite/coqchk/univ.v | 20 |
2 files changed, 32 insertions, 1 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5cb38cb81..5c672d04a 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -303,7 +303,18 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in - (*Start by checking types*) + (*Start by checking universes *) + let env = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> env + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + check_polymorphic_instance error env auctx1 auctx2 + | Monomorphic_const _, Polymorphic_const _ -> + error () + | Polymorphic_const _, Monomorphic_const _ -> + error () + in + (* Now check types *) let typ1 = cb1.const_type in let typ2 = cb2.const_type in check_type env typ1 typ2; diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index fcd740927..43815b61e 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -59,3 +59,23 @@ Module CMP_CON. Definition yo : foo@{U} = foo@{V} := eq_refl. End CMP_CON. + +Set Universe Polymorphism. + +Module POLY_SUBTYP. + + Module Type T. + Axiom foo : Type. + Parameter bar@{u v|u = v} : foo@{u}. + End T. + + Module M. + Axiom foo : Type. + Axiom bar@{u v|u = v} : foo@{v}. + End M. + + Module F (A:T). End F. + + Module X := F M. + +End POLY_SUBTYP. |