Using the lack of strict positivity to run an infinite computation

Negative.idr

data EventT : (event : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  MkEventTCont : (event -> m (EventT event m a)) -> EventT event m a
  MkEventTTerm : m a -> EventT event m a
  MkEventTEmpty : EventT event m a

data LAM : (x : Type) -> Type where
  App : x -> x -> LAM x
  Lam : (x -> x) -> LAM x

LC : Type
LC = EventT () LAM Void

app : LC -> LC -> LC
app f t = MkEventTCont (\ () => App f t)

lam : (LC -> LC) -> LC
lam b = MkEventTCont (\ () => Lam b)

delta : LC
delta = lam (\ x => app x x)

omega : LC
omega = app delta delta

reduce : LC -> LC
reduce lc@(MkEventTCont e) = case e () of
  App (MkEventTCont f) t => case f () of
    Lam b => reduce (b t)
    _     => lc
  _ => lc
reduce lc = lc

-- good luck running `reduce omega`!