[Agda] Using coinductive record constructor fails termination checking (2.5.1.1)

[Sebastian Seufert]

Dear all,

I have a record declared that is parametrized with Stream Set:

record ⟦_⟧ (R : Stream Set)  {i : Size} : Set where 
  coinductive
  constructor _►_   
  field
    now   : hd R 
    later :  ∀ {j : Size< i} → ⟦ tl R ⟧ {j}
open ⟦_⟧ public

Using the record with copatterns is fine by the termination checker :

foo : ⟦ repeat ℕ  ⟧ 
now foo = 0
later foo = foo

whereas using the constructor awakens the termination-check-dogs:

bar : ⟦ repeat ℕ ⟧
bar = 0 ► bar

--

Stream is defined using sized types 

record Stream {i : Size} {a} (A : Set a) : Set a where
  coinductive
  constructor _∷_
  field
    hd : A
    tl : ∀ {j : Size< i} → Stream {j} A
open Stream public

and repeat like this

repeat : ∀ {a} {A : Set a} → A → Stream A
hd (repeat x) = x
tl (repeat x) = repeat x

I expected the behaviour of foo to be the same as bar, wondering if there's something I am missing.

Regards,
-Sebastian