{-# OPTIONS --guardedness #-}

module DataRecordCoinductive where

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

mutual

  data Stream (A : Set) : Set where
    cons : Cons A → Stream A

  -- since Cons is coinductive, we are creating streams
  record Cons (A : Set) : Set where
    coinductive
    constructor _∷_
    field head : A
          tail : Stream A

open Cons

mutual

  repeat : {A : Set}(a : A) → Stream A
  repeat a = cons (repeat' a)

  repeat'  : {A : Set}(a : A) → Cons A
  head (repeat' a) = a
  tail (repeat' a) = repeat a

-- should not termination check: coconstructors are not size preserving
consume : {A : Set} → Stream A → ⊥
-- consume (cons s) = consume (tail s)  -- fails termination check
consume (cons (x ∷ xs)) = consume xs

loop : ⊥
loop = consume (repeat tt)
