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.)
---
 pretyping/inferCumulativity.ml | 2 +-
 test-suite/bugs/closed/8288.v  | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/8288.v

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index eb283a0220..be79b8b07d 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
   | FEvar ((_,args),e) ->
     let variances = infer_stack infos variances stk in
     infer_vect infos variances (Array.map (mk_clos e) args)
-  | FRel _ -> variances
+  | FRel _ -> infer_stack infos variances stk
   | FFlex fl ->
     let variances = infer_table_key infos variances fl in
     infer_stack infos variances stk
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