{-# OPTIONS --sized-types #-}

module Fix where

open import Agda.Builtin.Size
open import Agda.Primitive

private variable
  a : Level

record Thunk (F : Size → Set a) i : Set a where
  coinductive
  field force : {j : Size< i} → F j

open Thunk

data Embed : ∀ {i} → Thunk (λ _ → Set) i → Set where
  [_] : ∀ {i A} → force A → Embed {↑ i} A

expel : {A : Thunk (λ _ → Set) ∞} → Embed A → force A
expel [ x ] = x

Fix′ : Size → (Set → Set) → Set
Fix′ i F = F (Embed {i} λ where .force {j} → Fix′ j F)

Fix = Fix′ ∞

data ⊥ : Set where

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()

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

app : Fix Bad → Fix Bad → ⊥
app (bad f) x = f [ x ]

self : Fix Bad
self = bad λ x → app (expel x) (expel x)

example : ⊥
example = app self self