{-#  OPTIONS --type-in-type #-}
module TarmoTree where

open import Coinduction hiding (fold)
open import Data.Bool hiding (T)

infix 4 _∷_

data L (X : Set) : Set where
  [] : L X
  _∷_ : X → ∞ (L X) → L X

map : ∀ {X Y} → (X → Y) → L X → L Y
map f [] = []
map f (x ∷ xs) = f x ∷ ♯ (map f (♭ xs))

data T : Set where
  node' : ∀ {X} → (X → T) → L X → T

node : L T → T
node = node' (λ x → x)

fold' : ∀ {X} → (∀ {Y} → (Y → X) → L Y → X) → T → X
fold' f (node' g ys) = f (λ x → fold' f (g x)) ys

fold : ∀ {X} → (L X → X) → T → X
fold f = fold' (λ g ys → f (map g ys))

data Unit : Set where
  tt : Unit

falg : L Unit → Unit
falg [] = tt
falg (y ∷ ♯ []) = tt
falg (y ∷ ♯ (y' ∷ y0)) = y'

f : T → Unit
f = fold falg

{-
bad : T
bad = node (node [] ∷ ♯ (bad ∷ ♯ []))
-}

bad : T
bad = node' (λ x → x) (node [] ∷ ♯ (bad ∷ ♯ []))

-- f bad