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

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.

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.

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

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.

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