diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-20 00:27:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:29:06 +0100 |
| commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
| tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 /test-suite/success | |
| parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) | |
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.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/cumulativity.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 0394ea340..dfa305dc6 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. |