test.agda

open import Size

mutual
  data Delay (A : Set) (i : Size) : Set where
    now   : A → Delay A i
    later : ∞Delay A i → Delay A i

  record ∞Delay (A : Set) (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → Delay A j
open ∞Delay public

never : ∀ {i A} → Delay A i
never {i} = later λ where .force {j} → never {i}

_ : Size< ∞
_ = ∞

never' : ∀ {A} → Delay A ∞
never' = later λ where .force → never'