Gibt es ein nicht-triviales Beispiel mit Uneinheitlichkeit des Universums in Idris?

Question

Ich habe eine question über Idris Art der Typüberprüfung von Universen gefragt. Jetzt versuche ich ein Beispiel, das Uneinheitlichkeit des Universums verursachen würde. Hier ist die einfachste, ich könnte kommen mit

foo : Type 
foo = Type 

bar : Main.foo 
bar = Main.foo 

Der Ausgang Fehler ist:

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} 

Anders als das obige Beispiel, gibt es reale Beispiele, die Universum Inkonsistenz verursachen? Warum sind sie inkonsistent?

Answer 1

Woran ich denken kann, ist das Paradox von Girard, das Uneinheitlichkeit des Universums verursacht. Allerdings kann ich mir kein reales Beispiel vorstellen, das Uneinheitlichkeit im Universum verwendet.

Answer 2

Es gibt diese eine aus der Testsuite:

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

Ich denke, es ist ziemlich schwer, aber :) diese Art der Sache durch Zufall zu tun.