From db0918bfa5089f9ab44374504cbd0ddc758ea1e5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Feb 2018 00:27:40 +0100
Subject: Cumulativity: improve treatment of irrelevant universes.

In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
---
 test-suite/success/cumulativity.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 0394ea340a..dfa305dc6e 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -115,3 +115,16 @@ Definition checkcumul :=
 (* They can only be compared at the highest type *)
 Fail Definition checkcumul' :=
   eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
+
+(* An inductive type with an irrelevant universe *)
+Inductive foo@{i} : Type@{i} := mkfoo { }.
+
+Definition bar := foo.
+
+(* The universe on mkfoo is flexible and should be unified with i. *)
+Definition foo1@{i} : foo@{i} := let x := mkfoo in x. (* fast path for conversion *)
+Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *)
+
+(* Rigid universes however should not be unified unnecessarily. *)
+Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x.
+Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x.
-- 
cgit v1.2.3