伊德里斯是否存在宇宙不一致的非常重要的例子？

Question

我问过question关于伊德里斯的类型检查宇宙的方法。现在我正在尝试一些会导致宇宙不一致的例子。这是我能想到的最简单的一个

foo : Type
foo = Type

bar : Main.foo
bar = Main.foo

输出错误是：

test.idr:2:5:Universe inconsistency.
        Working on: z
        Old domain: (4,4)
        New domain: (4,3)
        Involved constraints: 
                ConstraintFC {uconstraint = z <= w, ufc = test.idr:2:5}
                ConstraintFC {uconstraint = y < z, ufc = test.idr:2:5}
                ConstraintFC {uconstraint = z <= w, ufc = test.idr:2:5}

除了上面的例子，还有更多真正的例子导致宇宙不一致吗？为什么他们不一致？

Answer 1

测试套件中有一个：

https://github.com/idris-lang/Idris-dev/blob/master/test/universes002/universes002.idr

虽然我认为很难做到这种事情:)

Answer 2

我能想到的是吉拉德的悖论，它导致了宇宙的不一致。但是，我想不出任何利用宇宙不一致性的现实世界的例子。

Answer 3

在我的一个durp时刻，我想出的一个是

equalTypesCommute -> x=y -> (x=y)=(y=x)
equalTypesCommute Refl = Refl

这当然会爆炸:)