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> 

[yallop]

In fact, the following simpler program suffers from the same issue:

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

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

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

total
Omega : Void
Omega = app omega omega

[gallais]

That last one is properly rejected if you use %default total.

The totality checker somehow forgets to check that D is positive despite being in Omega's dependency graph. I've tried to track down this issue in the past but haven't found where the problem is.

[balint99]

In Agda, this piece of code is rejected because the universe of the type of the constructor Abs is Set_1, which is higher than Set_0, the universe of the data type itself. Therefore, I think that adding universe levels to Idris might solve this problem, provided that data type definitions like this are rejected.

[andrevidela]

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

still causes problems

[spcfox]

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

This data is incorrect if there are levels of universes. But in Agda it is also rejected by the positivity checker.

[spcfox]

Another example with incorrect positivity checking. In this example there are no problems with levels of universes. But T' should be erased

%default total

T : Type -> Type
T a = a -> Void

data D : Type

0 T' : () -> Type
T' () = T D

data D : Type where
  Abs : {default () x : ()} -> T' x -> D

app : D -> D -> Void
app $ Abs {x=()} f = f

omega : D
omega = Abs $ \x => app x x

boom : Void
boom = app omega omega