From 6c1783de49e0b11f65cc511a94e9ce37f7210562 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 Aug 2018 20:05:42 +0200
Subject: Fix #8288: cumulativity inferance ignores args to bound variables

(NB: only variables whose binder is inside the constructor argument,
ie

        Inductive foo := C : forall A : Type -> Type, A Type -> foo.

does not trigger the bug because A becomes a RelKey.)
---
 test-suite/bugs/closed/8288.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/8288.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v
new file mode 100644
index 0000000000..0350be9c06
--- /dev/null
+++ b/test-suite/bugs/closed/8288.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Set Polymorphic Inductive Cumulativity.
+
+Inductive foo := C : (forall A : Type -> Type, A Type) -> foo.
+(* anomaly invalid subtyping relation *)
-- 
cgit v1.2.3