Add regression tests for univ. poly. and prim proj

These regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently passes.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_025.v b/test-suite/bugs/closed/HoTT_coq_025.v
new file mode 100644
index 000000000..b81b454d0
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_025.v
@@ -0,0 +1,29 @@
+Module monomorphic.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+  (* Error: In environment
+A : Type
+B : Type
+iA : Inhabited A
+iB : Inhabited B
+The term "(A * B)%type" has type "Type" while it is expected to have type
+"Prop". *)
+End monomorphic.
+
+Module polymorphic.
+  Set Universe Polymorphism.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+End polymorphic.