Termination checking prefers `data` to `record`

[lawcho]

Termination checking prefers `data` to `record`

[andreasabel]

It should work if you put no-eta-equality.
With eta, foldSS is not terminating due to the record pattern translation which turns this into

foldSS f s = f (head s) (foldSS f (tail s))

[lawcho]

This passes:

record SillyStream (A : Set) : Set where
  inductive; pattern; constructor _∷_
  field head : A
  field tail : SillyStream A

foldSS : {A r : Set} → (A → r → r) → SillyStream A → r
foldSS f (head ∷ tail)  = f head (foldSS f tail)

[andreasabel]

Yes, because eta is off. This gives an error:

...
module _ (A : Set) (s : SillyStream A) where

  eta : s ≡ head s ∷ tail s
  eta = refl

[lawcho]

It seems like pattern is enough to get data-style checking of a record.

I don't think a doc update is required, since the pattern keyword is discoverable via Agda's error message:

/tmp/tmp.O6kGsXwZPr/tmp.agda:8,11-22
Pattern matching on no-eta record type SillyStream
(defined at /tmp/tmp.O6kGsXwZPr/tmp.agda:2,8-19) is not allowed
(to activate, add declaration `pattern` to record definition)
when checking that the pattern head ∷ tail has type SillyStream A

which arises when I give a naive translation of the data type:

record SillyStream (A : Set) : Set where
  inductive; constructor _∷_
  field head : A
  field tail : SillyStream A

(Agda version 422b932 of master)