Unguarded eta records can make Agda loop

[andreasabel]

From: https://github.com/agda/agda/issues/7467#issuecomment-2326548333

data ⊥ : Set where

record R : Set where
  eta-equality; inductive
  field f : R

f : R → ⊥
f ()       -- Agda loops here

From https://github.com/agda/agda/issues/7467#issuecomment-2327123945

open import Agda.Builtin.Equality

record R : Set where
  eta-equality; inductive
  field f : R

open R

loop : (let X = _) → X .f ≡ X .f → Set
loop refl = {!!}  -- type checker loops

So far our policy was: if the user writes eta-equality explicitly, they understand the risks. However, judging from @UlfNorell 's reaction in https://github.com/agda/agda/issues/7467#issuecomment-2327123945, this might not be the case.

So we would like to issue a warning, possibly make this an error, possibly make this not --safe.

What complicates the situation is that the check (positivity) that detects the potential unsafety runs only at the end of mutual blocks. So we could issue the warning only then.

1. This could be too late anyway, as Agda might already have diverged using the stipulated eta-equality for the record type.
2. If we switch off eta after the fact (as in current PR #7470), we could lose subject reduction as eta has been available inside the mutual block but is not available after the check.
3. So we can for instance just warn about it. This would be the least invasive change. Would also mean that --safe does not prevent Agda from looping (doesn't anyway always, see 1.).
4. Or we make this an error with --safe. In this case, we need to change the standard library as in https://github.com/agda/agda-stdlib/pull/2476.
5. In #7470 one can use the ETA pragma to force eta pragma even if Agda has doubts, but it is not --safe.

[andreasabel]

Agda dev meeting 2024-09-11: make ETA safe