Termination checking prefers data to record

[lawcho]

foldSS passes when data is used, but not when record is used:

-- Fails syntax-based termination checking
record SillyStream (A : Set) : Set where
  inductive; eta-equality; constructor _∷_
  field head : A
  field tail : SillyStream A

-- -- Passes syntax-based termination checking
-- data SillyStream (A : Set) : Set where
--   _∷_
--     : (head : A)
--     → SillyStream A
--     → SillyStream A

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

I expected syntax-based termination to spot the structural recursion either way.

Agda Versions tested

• Bug present in 422b932 of master
• Bug present in 637ae08 of Add type-based termination checker #7152 (with TBT turned off)
• Bug absent in 637ae08 of Add type-based termination checker #7152 (with TBT turned on)

[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)