diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-13 14:16:49 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-22 13:09:16 +0200 |
commit | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (patch) | |
tree | b583fda3032bb363ce85dd621fcd41f7fb9d98f1 /test-suite/bugs | |
parent | d236c7362053c4fc8f1c7f3b59248b412b029fb8 (diff) |
Remove hack skipping comparison of algebraic universes in subtyping.
When inferring [u <= v+k] I replaced the exception and instead add
[u <= v]. This is trivially sound and it doesn't seem possible to have
the one without the other (except specially for [Set <= v+k] which was
already handled).
I don't know an example where this used to fail and now succeeds (the
point was to remove an anomaly, but the example
~~~
Module Type SG. Definition DG := Type. End SG.
Module MG : SG. Definition DG := Type : Type. Fail End MG.
~~~
now fails with universe inconsistency.
Fix #7695 (soundness bug!).
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/7695.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v new file mode 100644 index 000000000..42bdb076b --- /dev/null +++ b/test-suite/bugs/closed/7695.v @@ -0,0 +1,20 @@ +Require Import Hurkens. + +Universes i j k. +Module Type T. + Parameter T1 : Type@{i+1}. + Parameter e : Type@{j} = T1 : Type@{k}. +End T. + +Module M. + Definition T1 := Type@{j}. + Definition e : Type@{j} = T1 : Type@{k} := eq_refl. +End M. + +Module F (A:T). + Definition bad := TypeNeqSmallType.paradox _ A.e. +End F. + +Set Printing Universes. +Fail Module X := F M. +(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *) |