diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3352.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3352.v')
-rw-r--r-- | test-suite/bugs/closed/3352.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v new file mode 100644 index 00000000..b57b0a0f --- /dev/null +++ b/test-suite/bugs/closed/3352.v @@ -0,0 +1,34 @@ + +(* +I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo]. (I think this worked in HoTT/coq, too.) Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A]. (The issue is tricker when IsHProp uses [A] elsewhere, as in: +*) + +(* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) +Set Universe Polymorphism. +Inductive Empty : Set := . +Record IsHProp (A : Type) := { foo : True }. +Definition hprop_Empty : IsHProp@{i} Empty := {| foo := I |}. +Goal let U := Type in let gt := Set : U in IsHProp (Empty : U). +simpl. +Set Printing Universes. +exact @hprop_Empty. (* Toplevel input, characters 21-32: +Error: +The term "hprop_Empty" has type "IsHProp (* Set *) Empty" +while it is expected to have type "IsHProp (* Top.17 *) Empty" +(Universe inconsistency: Cannot enforce Top.17 = Set because Set < Top.17)). *) +Defined. + +Module B. +(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) +Set Universe Polymorphism. +Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Record Contr (A : Type) := { center : A }. +Monomorphic Record IsHProp (A : Type) := { foo : forall x y : A, Contr (x = y) }. +Definition hprop_Empty : IsHProp Empty := {| foo x y := match x : Empty with end |}. +Goal let U := Type in let gt := Set : U in IsHProp (Empty : U). +simpl. +Set Printing Universes. +exact hprop_Empty. +Defined. +End B.
\ No newline at end of file |