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

diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
new file mode 100644
index 000000000..a14fb6aa5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -0,0 +1,50 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Set Printing Universes.
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Inductive Unit : Type :=
+    tt : Unit.
+
+Inductive Bool : Type :=
+  | true : Bool
+  | false : Bool.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Record PreCategory :=
+  {
+    Object :> Type;
+    Morphism : Object -> Object -> Type
+  }.
+
+Definition DiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                        (@paths X).
+
+Definition IndiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                         (fun _ _ => Unit).
+
+Definition NatCategory (n : nat) :=
+  match n with
+    | 0 => IndiscreteCategory Unit
+    | _ => DiscreteCategory Bool
+  end.
+(* Error: Universe inconsistency (cannot enforce Set <= Prop).*)
+
+Definition NatCategory' (n : nat) :=
+  match n with
+    | 0 => (fun X => @Build_PreCategory X
+                         (fun _ _ => Unit : Prop)) Unit
+    | _ => DiscreteCategory Bool
+  end.
+
+Definition NatCategory'' (n : nat) :=
+  match n with
+    | 0 => IndiscreteCategory Unit
+    | _ => DiscreteCategory Bool
+  end.