[Agda] productivity of fibonacci stream

[Noam Zeilberger]

Hello Agda List,

This might be a FAQ, but I was wondering why the canonical
implementation of the stream of Fibonacci numbers using copatterns
does not pass Agda's termination checker? By "canonical
implementation" (cf. section 2.3 of
http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf), I mean the following:

====
open import Agda.Builtin.Nat public

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A
open Stream

zipWith : {A B C : Set} → (A → B → C) → Stream A → Stream B → Stream C
hd (zipWith f xs ys) = f (hd xs) (hd ys)
tl (zipWith f xs ys) = zipWith f (tl xs) (tl ys)

fib : Stream Nat
hd fib = 0
hd (tl fib) = 1
tl (tl fib) = zipWith _+_ fib (tl fib)
====

which yields the following warning:
====
Termination checking failed for the following functions:
  fib
Problematic calls:
  fib
    (at .../Fib.agda:19,27-30)
  tl fib
    (at .../Fib.agda:19,35-38)
====

Any hints as to why Agda is complaining?

Noam