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.

4 files changed, 90 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_074.v b/test-suite/bugs/opened/HoTT_coq_074.v
new file mode 100644
index 0000000000..7c88447b29
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_074.v
@@ -0,0 +1,12 @@
+Monomorphic Definition U1 := Type.
+Monomorphic Definition U2 := Type.
+
+Set Printing Universes.
+Definition foo : True.
+Fail let t1 := type of U1 in
+let t2 := type of U2 in
+pose (t1 : t2). (* Error:
+The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)"
+while it is expected to have type "Type (* Top.2+1 *)". *)
+exact I.
+Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_077.v b/test-suite/bugs/opened/HoTT_coq_077.v
new file mode 100644
index 0000000000..68d3056619
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_077.v
@@ -0,0 +1,39 @@
+Set Implicit Arguments.
+
+Require Import Logic.
+
+Set Asymmetric Patterns.
+Set Record Elimination Schemes.
+Set Primitive Projections.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Print prod_rect.
+(** prod_rect =
+fun (A B : Type) (P : prod A B -> Type)
+  (f : forall (fst : A) (snd : B), P {| fst := fst; snd := snd |})
+  (p : prod A B) =>
+match p as p0 return (P p0) with
+| {| fst := x; snd := x0 |} => f x x0
+end
+     : forall (A B : Type) (P : prod A B -> Type),
+       (forall (fst : A) (snd : B), P {| fst := fst; snd := snd |}) ->
+       forall p : prod A B, P p
+
+Arguments A, B are implicit
+Argument scopes are [type_scope type_scope _ _ _]
+ *)
+
+(* What I really want: *)
+Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
+           (p : prod A B) : P p
+  := u (fst p) (snd p).
+
+Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
+
+(* Check for eta *)
+Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
+
+(* Check for the recursion principle I want *)
+Fail Check eq_refl : @prod_rect = @prod_rect'.
diff --git a/test-suite/bugs/opened/HoTT_coq_093.v b/test-suite/bugs/opened/HoTT_coq_093.v
new file mode 100644
index 0000000000..029a0caf76
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_093.v
@@ -0,0 +1,37 @@
+(** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
+Set Printing All.
+Set Printing Implicit.
+Set Printing Universes.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Section lift.
+  Let lift_type : Type.
+  Proof.
+    let U0 := constr:(Type) in
+    let U1 := constr:(Type) in
+    let unif := constr:(U0 : U1) in
+    exact (U0 -> U1).
+  Defined.
+
+  Definition Lift : lift_type := fun A => A.
+End lift.
+
+Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y.
+intros A x y p.
+compute in *.
+Fail exact p. (* Toplevel input, characters 21-22:
+Error:
+In environment
+A : Type (* Top.15 *)
+x : A
+y : A
+p : @paths (* Top.15 *) A x y
+The term "p" has type "@paths (* Top.15 *) A x y"
+while it is expected to have type "@paths (* Top.18 *) A x y"
+(Universe inconsistency: Cannot enforce Top.18 = Top.15 because Top.15
+< Top.18)). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_114.v b/test-suite/bugs/opened/HoTT_coq_114.v
new file mode 100644
index 0000000000..e293e6dbbb
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_114.v
@@ -0,0 +1,2 @@
+Fail Inductive test : $(let U := type of Type in exact U)$ := t.
+(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *)