Higher constructors can trick the productivity checker

[dolio]

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.

[nad]

Here is a self-contained test case:

{-# OPTIONS --safe --cubical --guardedness #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

mutual

  record R : Set where
    coinductive
    field
      force : D

  data D : Set where
    point  : R → D
    higher : R.force ≡ point

r : R
r .R.force = higher i0 r

loops : D
loops = r .R.force