diff options
author | 2014-04-08 01:42:49 -0400 | |
---|---|---|
committer | 2014-05-10 15:39:30 +0200 | |
commit | 3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (patch) | |
tree | b3a938d606daa421a6e8d566d69fdc93b99f88fd /test-suite/bugs/closed/HoTT_coq_089.v | |
parent | 3507f3d81082f5f4aef165cc3f4b0207224fb0cb (diff) |
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.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_089.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_089.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_089.v b/test-suite/bugs/closed/HoTT_coq_089.v new file mode 100644 index 000000000..54ae4704a --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_089.v @@ -0,0 +1,42 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Inductive type_paths (A : Type) : Type -> Prop + := idtypepath : type_paths A A. +Monomorphic Definition comp_type_paths := Eval compute in type_paths. +Check comp_type_paths. +(* comp_type_paths + : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *) +(* This is terrible. *) + +Inductive type_paths' (A : Type) : Type -> Prop + := idtypepath' : type_paths' A A + | other_type_path : False -> forall B : Set, type_paths' A B. +Monomorphic Definition comp_type_paths' := Eval compute in type_paths'. +Check comp_type_paths'. +(* comp_type_paths' + : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *) +(* Ok, then ... *) + +(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *) +Goal Type. +Proof. + match type of comp_type_paths' with + | ?U0 -> ?U1 -> ?R + => exact (@comp_type_paths' nat U0) + end. +Defined. + +Goal Type. +Proof. + match type of comp_type_paths with + | ?U0 -> ?U1 -> ?R + => exact (@comp_type_paths nat U0) + end. + (* Toplevel input, characters 110-112: +Error: +The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)" +while it is expected to have type "Type (* Top.51 *)" +(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51 += Top.51)). *) +Defined. |