aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-03 22:20:30 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-03 22:20:30 +0100
commitc135410086c256fcc74f579459687a83718148b9 (patch)
tree3a674c331640d4fb61c3d6eef28c15810988785a
parent2d3916766d3f145643a994aa83174c98394d5baa (diff)
Fix test-suite file, this is currently a wontfix, but keep the
test-suite file for when we move to a better implementation.
-rw-r--r--test-suite/bugs/closed/3690.v52
1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
new file mode 100644
index 000000000..4069e3807
--- /dev/null
+++ b/test-suite/bugs/closed/3690.v
@@ -0,0 +1,52 @@
+Set Printing Universes.
+Set Universe Polymorphism.
+Definition foo (a := Type) (b := Type) (c := Type) := Type.
+Print foo.
+(* foo =
+let a := Type@{Top.1} in
+let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
+ : Type@{Top.4+1}
+(* Top.1
+ Top.2
+ Top.3
+ Top.4 |= *) *)
+Check @foo. (* foo@{Top.5 Top.6 Top.7
+Top.8}
+ : Type@{Top.8+1}
+(* Top.5
+ Top.6
+ Top.7
+ Top.8 |= *) *)
+Definition bar := $(let t := eval compute in foo in exact t)$.
+Check @bar. (* bar@{Top.13 Top.14 Top.15
+Top.16}
+ : Type@{Top.16+1}
+(* Top.13
+ Top.14
+ Top.15
+ Top.16 |= *) *)
+(* The following should fail, since [bar] should only need one universe. *)
+Check @bar@{i j}.
+Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
+Definition qux := Eval compute in baz.
+Check @qux. (* qux@{Top.24 Top.25
+Top.26}
+ : Type@{max(Top.24+1, Top.26+1)}
+(* Top.24
+ Top.25
+ Top.26 |= Top.25 < Top.24
+ Top.26 < Top.25
+ *) *)
+Print qux. (* qux =
+Type@{Top.21} -> Type@{Top.23}
+ : Type@{max(Top.21+1, Top.23+1)}
+(* Top.21
+ Top.22
+ Top.23 |= Top.22 < Top.21
+ Top.23 < Top.22
+ *) *)
+Fail Check @qux@{Set Set}.
+Fail Check @qux@{Set Set Set}.
+(* [qux] should only need two universes *)
+Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *)
+Fail Check @qux@{i j}.