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

diff --git a/test-suite/bugs/closed/HoTT_coq_044.v b/test-suite/bugs/closed/HoTT_coq_044.v
new file mode 100644
index 000000000..1a59de092
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_044.v
@@ -0,0 +1,32 @@
+Require Import Classes.RelationClasses List Setoid.
+
+Set Universe Polymorphism.
+
+Definition RowType := list Type.
+
+
+Inductive Row : RowType -> Type :=
+| RNil : Row nil
+| RCons : forall T Ts, T -> Row Ts -> Row (T :: Ts).
+
+Inductive RowTypeDecidable (P : forall T, relation T) `(H : forall T, Equivalence (P T))
+: RowType -> Type :=
+| RTDecNil : RowTypeDecidable P H nil
+| RTDecCons : forall T Ts, (forall t0 t1 : T,
+                              {P T t0 t1} + {~P T t0 t1})
+                           -> RowTypeDecidable P H Ts
+                           -> RowTypeDecidable P H (T :: Ts).
+
+Set Printing Universes.
+
+Fixpoint Row_eq Ts
+: RowTypeDecidable (@eq) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}.
+(* Toplevel input, characters 81-87:
+Error:
+In environment
+Ts : RowType (* Top.53 Coq.Init.Logic.8 *)
+r1 : Row (* Top.54 Top.55 *) Ts
+r2 : Row (* Top.56 Top.57 *) Ts
+The term "Row (* Coq.Init.Logic.8 Top.59 *) Ts" has type
+ "Type (* max(Top.58+1, Top.59) *)" while it is expected to have type
+ "Type (* Coq.Init.Logic.8 *)" (Universe inconsistency). *)