[Agda] Termination checking failure

[Ivan Tomac]

Nils Anders Danielsson wrote:
>
> The following code works:
>
>  map : ∀ {A B} → (A → B) → Stream A → Stream B
>  map f (cons x xs) = cons (f x) (♯ map f (♭ xs))
>
>  sequence : ∀ {A} → Stream (Id A) → Id (Stream A)
>  sequence = id ∘ map unId
>
Yes, that does work for that particular case. I should have been a bit 
more clear though. The code here is simplified version of the problem I 
ran into before where the above wouldn't work. What happens in a more 
general case for example with an applicative functor instead of Id:

sequence : ∀ {F a} → RawApplicative F → Stream (F a) → F (Stream a)
sequence A (cons f fs) =
    cons <$> f ⊛ ((λ as → ♯ as) <$> sequence A (♭ fs))
    where
    open RawApplicative A
>> And why is the termination checker failing in first place?
>
> Because the corecursive call is not guarded by constructors.
>
>> I would appreciate any pointers to papers, articles or books.
>
> You may want to have a look at "Mixing Induction and Coinduction":
>
>  http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html 
>
>
Thanks for the link. I'll have a read through it.