From 5af5bff88fa49731acbf24d8a67148e4215446bd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 22 Apr 2018 16:51:25 +0200
Subject: Fix #7327: coqchk subtyping of polymorphic constants

---
 checker/subtyping.ml     | 13 ++++++++++++-
 test-suite/coqchk/univ.v | 20 ++++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

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.
-- 
cgit v1.2.3