Add more regression tests for univ poly/prim proj

hese 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 fails.

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, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v
new file mode 100644
index 000000000..36f478002
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_080.v
@@ -0,0 +1,34 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+
+Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
+Inductive Empty :=.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+Set Printing All.
+Definition sum_category (C D : category) : category :=
+  {|
+    ob := sum (ob C) (ob D);
+    hom x y := match x, y with
+                 | inl x, inl y => @hom C x y
+                 | inr x, inr y => @hom D x y
+                 | _, _ => Empty
+               end |}.
+
+Goal forall C D (x y : ob (sum_category C D)), Type.
+intros C D x y.
+hnf in x, y.
+exact (hom x y). (* Toplevel input, characters 26-27:
+Error:
+In environment
+C : category
+D : category
+x : sum (ob C) (ob D)
+y : sum (ob C) (ob D)
+The term "x" has type "sum (ob C) (ob D)" while it is expected to have type
+ "ob ?16". *)