Singleton check loops on recursive eta record

[oisdk]

The following code loops in Agda 2.6.2.1:

record Acc {a r} {A : Type a} (R : A → A → Type r) (x : A) : Type (a ℓ⊔ r) where
  inductive; eta-equality
  constructor acc
  field step : ∀ y → R y x → Acc R y
open Acc public

isPropAcc : ∀ {r} {R : A → A → Type r} {x : A} → isProp (Acc R x)
isPropAcc (acc x) (acc y) = cong acc (funExt λ n → funExt λ p → isPropAcc (x n p) (y n p))

It uses a recursive inductive record (the Acc type for well-founded recursion), and tries to prove a property on it by recursing over it.

I am not sure if this behaviour is expected (it goes away if eta-equality is replaced by pattern), but the manual seems to suggest that this code should be safe.

[andreasabel]

Agda loops when trying to check whether Acc R x is a singleton; it unfolds forever:

considering eta-expansion at type
Acc (_R_83 (x = x₄) (y = y₂)) y₃

Is Acc (_R_83 (x = x₄) (y = y₂)) y₃ a singleton record type?
isSingletonRecord' checking telescope  (step₁
                                        : (y₄ : _A_82 (x = x₄) (y = y₂)) →
                                          _R_83 (x = x₄) (y = y₂) y₄ y₃ →
                                          Acc (_R_83 (x = x₄) (y = y₂)) y₄)
Is Acc (_R_83 (x = x₄) (y = y₂)) y₄ a singleton record type?
...

[andreasabel]

Congrats, @oisdk, you found a bug that has been open since Agda 2.5.1.1!
It is fixed on #5824, and now you get the termination error you deserve instead. (Can't recurse on a eta record type!)

[andreasabel]

Here is a MWE that makes Agda loop (since Agda 2.5.1.1, when eta-equality was added):

record Empty : Set where
  inductive; eta-equality
  field out : Empty

test : Empty
test = _