diff options
author | 2014-06-17 17:03:25 +0200 | |
---|---|---|
committer | 2014-06-17 17:19:04 +0200 | |
commit | 40c2154e369cf1a3434fe34679bb3a186df3199a (patch) | |
tree | 81118ebda2f219e840dcf24bb6d3b32fb2d24e34 /test-suite/bugs/closed/HoTT_coq_089.v | |
parent | bd755284f3fcdf7f2fced477b81d64d72226a38f (diff) |
Not considering test-suite file #89 as a bug anymore.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_089.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_089.v | 43 |
1 files changed, 43 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..6841d6b27 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_089.v @@ -0,0 +1,43 @@ +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@{Type Type}. +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 : Type, 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. |