{-# OPTIONS --no-positivity-check #-}

data ⊥ : Set where

data Bad : Set where
  bad : (Bad → ⊥) → Bad

app : Bad → ⊥
app (bad f) = f (bad f)

uhoh : ⊥
uhoh = app (bad app)