[Agda] Agda goes coinductive

[Dan Doel]

On Thursday 05 June 2008, Dan Doel wrote:
> data _↓_ {a : Set} : D a -> a -> Set where
>   convergeNow   : {x : a} -> (now x) ↓ x
>   convergeLater : {x : a} {dx : D a} -> dx ↓ x -> later dx ↓ x
>
> codata _↑ {a : Set} : D a -> Set where
>   diverge : {dx : D a} -> dx ↑ -> later dx ↑
>
> -- problems here
> -- diverge-never : never ↑
> -- diverge-never ~ diverge diverge-never
> -- complaint: never != later never

Sorry to reply to myself, but I've been working on converting more of the 
General Recursion via Coinductive Types proofs to Agda, and I think I've run 
into this again. For instance:

  mapD : {a b : Set} -> (a -> b) -> D a -> D b
  mapD f (now x)    = now (f x)
  mapD f (later dx) = later (mapD f dx)

This fails the termination checker (of course), but it allows me to write:

  map-↓ : {a b : Set} {f : a -> b}{x : D a}{v : a} -> x ↓ v -> mapD f x ↓ f v
  map-↓ convergeNow        = convergeNow
  map-↓ (convergeLater pf) = convergeLater (map-↓ pf)

If I change the =s in mapD to ~s, the productivity checker is satisfied, but 
now map-↓ (and similar definitions) complain, because it says

  map f (now v) != now (f v)

Is this to be expected, or is it an oversight?

Thanks.

-- Dan