[Agda] Termination checking failure

[Ivan Tomac]

Hi,

How would I go about rewriting the code in the attached file so that it 
passes termination checking? And why is the termination checker failing 
in first place?
I'm guessing it's probably due to my lack of understanding of 
coinduction and codata and how they are handled in Agda - from reading 
the Agda wiki and going through the standard libraries I thought this 
would work.
I would appreciate any pointers to papers, articles or books.

Ivan

-------------- next part --------------
module Test where

open import Coinduction

data Id (A : Set) : Set where
    id : A → Id A

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

unId : ∀ {A} → Id A → A
unId (id A) = A

sequence : ∀ {A} → Stream (Id A) → Id (Stream A)
sequence (cons (id a) is) = id (cons a (♯ unId (sequence (♭ is))))