Girards Paradox copied from Agda

[yokto]

If i just blindly translate the following program to Idris i get an endless loop. Idris doesn't seem to complain about it during compilation. agda gives a compilation error.

https://github.com/nzl-nott/PhD-of-nzl/blob/master/Exercise/Ex4/girard.agda

I don't claim to understand exactly what's happening here. Maybe I'm using some wrong options.

I just idris2 Pa.idr. And if i run loop Nat it seems an endless loop

Tried with idris2 0.7 from nix.

module Pa

-- copied https://github.com/nzl-nott/PhD-of-nzl/blob/master/Exercise/Ex4/girard.agda

%default total

PowerSet : Type -> Type
PowerSet t = t -> Type

PowerPowerSet : Type -> Type
PowerPowerSet t = PowerSet (PowerSet t) -- (t -> Type) -> Type

U : Type
U = (X : Type) -> ((PowerPowerSet X) -> X) -> (PowerPowerSet X)

tau : PowerPowerSet U -> U
tau ppsetU typeX ppToX xToType = ppsetU (\x => xToType (ppToX (x typeX ppToX)))

Sigma : U -> PowerPowerSet U
Sigma universe = universe U (\t => tau t)

Bottom : Type
Bottom = (t: Type) -> t

No : Type -> Type
No wrongType = wrongType -> Bottom

delta : PowerSet U
delta universe = No ((p : PowerSet U) -> Sigma universe p -> p (tau (Sigma universe)))

Ω : U
Ω = tau (\p => (x : U) -> Sigma x p -> p x)

D : Type
D = (p : PowerSet U) -> Sigma Ω p -> p (tau (Sigma Ω))

lem0 : (p : PowerSet U) -> ((x : U) -> Sigma x p -> p x) -> p Ω
lem0 p h1 = h1 Ω (\x => h1 (tau (Sigma x)))

lem2 : No D
lem2 = lem0 delta (\x => \h2 => \h3 => h3 delta h2 $ \p => h3 $ \y => p (tau (Sigma y)))

lem3 : D
lem3 p = lem0 (\y => p (tau (Sigma y)))

loop : Bottom
loop = lem2 lem3

[gallais]

That's expected given that Idris currently implements Type : Type and Girard's paradox was precisely about that rule in ML's 1971 system (cf. https://github.com/michaelt/martin-lof for a copy).