在 Idris 中是否有一个关于宇宙不一致的重要示例？答案

【问题标题】：Is there a non-trivial example with universe inconsistency in Idris?在 Idris 中是否有一个关于宇宙不一致的重要示例？
【发布时间】：2023-04-10 20:48:02
【问题描述】：

我已经向question 询问了有关 Idris 类型检查 Universe 的方式。现在我正在尝试一些会导致宇宙不一致的例子。这是我能想到的最简单的方法

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}

除了上面的例子，还有没有更真实的例子导致宇宙不一致？为什么它们不一致？

【问题讨论】：

标签： types idris

【解决方案1】：

测试套件中有这个：

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

我认为虽然偶然做这种事情是相当困难的:)。

【讨论】：

【解决方案2】：

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

【讨论】：

【解决方案3】：

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

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

当然，这会爆炸:)

【讨论】：

【解决方案4】：

我只是偶然发现了这一点。这是一个很自然的定义，所以真的很令人惊讶。

Subset : Type -> Type
Subset a = a -> Type

Family : Type -> Type
Family a = Subset (Subset a)

familyIntersection : Family a -> Subset a
familyIntersection {a} f x = (u : Subset a) -> f u -> u x

这给出了输出（对于idris --check）：

test.idr:2:12-20:
  |
2 | Subset a = a -> Type
  |            ~~~~~~~~~
Universe inconsistency.
        Working on: ./test.idr.l1
        Old domain: (4,4)
        New domain: (4,3)
        Involved constraints: 
                ConstraintFC {uconstraint = ./test.idr.l1 < ./test.idr.m1, ufc = test.idr:2:12-20}
                ConstraintFC {uconstraint = ./test.idr.l1 < ./test.idr.m1, ufc = test.idr:2:12-20}
                ConstraintFC {uconstraint = ./test.idr.v2 <= ./test.idr.l1, ufc = test.idr:8:30-57}

对于任何不熟悉的人来说，这是从集合论翻译（在我看来以最自然的方式）到 Idris 的基本定义：如果一个元素在所有子集的交集中，则它是子集族的交集。换句话说，如果对于基本类型的每个子集，如果子集在族中，则元素在交集中。

【讨论】：

【解决方案5】：

偶然发现的。如果您省略{ty: Type} ->，它会抱怨宇宙不一致。虽然不确定这不是编译器错误。

codata Conat = Z | S Conat

codata Covect : (len : Conat) -> ty -> Type where
  (::) :  ty -> Covect len ty -> Covect (S len) ty
  Nil  :  {ty: Type} -> Covect Z ty
  -- Nil  :  Covect Z ty       -- for some reason this messes with the universe 

stripe : Covect len (Covect len t) -> Covect len (List ty)
stripe [] = []

【讨论】：