Есть ли нетривиальный пример с несогласованностью Вселенной в Идрисе?

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

То, что я могу представить, это парадокс Жирарда, который вызывает вселенную несогласованности. Тем не менее, я не могу придумать какой-либо реальный пример мира, который использует вселенную несостоятельность atm.

Answer 2

Там эта одна из тестового набора:

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

Я думаю, что это довольно трудно сделать такую ​​вещь случайно, хотя :).