Implement module subtyping for polymorphic constants (errors on

inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.

1 files changed, 23 insertions, 0 deletions

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.