[Agda] My coinductive function doesn't termination-check

[Nick Smallbone]

Hi Agdaers,

I'm trying to use coinduction to model possibly-nonterminating
functions:

  module Delay where

  open import Coinduction

  data Delay (A : Set) : Set where
    now : A → Delay A
    later : ∞ (Delay A) → Delay A

  fix : ∀ {A} → (Delay A → Delay A) → Delay A
  fix f = later (♯ f (fix f))

The idea is that Delay A represents a computation that may eventually
produce a value of type A---or might not. As I understand it, fix is
productive, but it doesn't seem to termination-check. Why's that?

Nick