From d1a39e06c44dc451d8a56a286017885d400ac435 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 6 May 2014 09:51:21 -0400 Subject: 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. --- test-suite/bugs/closed/HoTT_coq_059.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_059.v (limited to 'test-suite/bugs/closed/HoTT_coq_059.v') diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v new file mode 100644 index 000000000..9c7e394dc --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -0,0 +1,17 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +Set Universe Polymorphism. + +Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x. +Notation "a = b" := (eq a b) : type_scope. + +Section foo. + Class Funext := { path_forall :> forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }. + Context `{Funext, Funext}. + + Set Printing Universes. + + (** Typeclass resolution should pick up the different instances of Funext automatically *) + Definition foo := (@path_forall _ _ _ (@path_forall _ Set)). + (* Toplevel input, characters 0-60: +Error: Universe inconsistency (cannot enforce Top.24 <= Top.23 because Top.23 +< Top.22 <= Top.24). *) -- cgit v1.2.3