Agda's productivity checker seems to be satisfied by a definition being guarded by higher constructors. However, higher constructors can reduce to non-constructors at their endpoints, allowing definitions like this to be accepted:

data C (A : Type) : Type

record P (A : Type) : Type where
  coinductive
  field
    force : C A

open P

data C A where
  now : A → C A
  later : P A → C A
  wait : force ≡ later

hmm : P A
hmm .force = wait i0 hmm

Normalizing force hmm is an infinite loop.

This example is wrong in an obvious way, because wait i0 = force, so the definition of hmm is actually equivalent to force hmm = force hmm. But, it'd be really nice if a proper understanding of how this should work also rules out P A being contractible:

∞ : P A
∞ .force = later ∞
  
contr : ∀(x : P A) → x ≡ ∞
contr x i .force = wait i (contr x i)

since this definition also contains, as a specialization:

contr x i0 .force = contr x i0 .force

Although in that case it evaluates like contr x i0 .force = x .force, so perhaps this is too much to hope for.