total Omega : ⊥

[yallop]

While trying to understand the differences between Agda's and Idris's positivity checkers, I came across Andreas Abel's message from 2012, which passes the totality checker when translated to Idris:

data D : Type where Abs : (D = e) -> (e -> Void) -> D

lam : (D -> Void) -> D
lam f = Abs Refl f

app : D -> D -> Void
app (Abs Refl f) d = f d

omega : D
omega = lam (\x => app x x)

total
Omega : Void
Omega = app omega omega

$ idris2 omega.idr 
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.4.0-5126600fa
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
1/1: Building omega (omega.idr)
Main> :total Omega
Main.Omega is total
Main>