corecursive Agda functions without sized types

Question

I've been doing some experiments with the "old" and "new" ways of dealing with coinduction in Agda, but I think I'm still missing some important facts about the behavior of Agda's termination checking of corecursive functions when Size is not used.

As an example, consider the following definitions of Stream and repeat:

data    Stream (A : Set) : Set
record ∞Stream (A : Set) : Set where
  coinductive
  field force : Stream A
open ∞Stream

data Stream A where
  cons : A -> ∞Stream A -> Stream A

repeat : ∀{A} -> A -> ∞Stream A
force (repeat x) = cons x (repeat x)

Roughly speaking, the coinductive record type ∞Stream is a specialized Thunk for streams. I've seen similar definitions in quite a few Agda formalizations, although they're usually refined a Size for better precision. Anyway, the above definition of repeat is accepted by Agda without any Size annotations.

The problem is when I try to factor out the ∞Stream record into a Thunk, so that I can reuse Thunk elsewhere for defining other potentially infinite data types:

record Thunk (A : Set) : Set where
  coinductive
  field force : A
open Thunk

data Stream (A : Set) : Set where
  cons : A -> Thunk (Stream A) -> Stream A

repeat : ∀{A} -> A -> Thunk (Stream A)
force (repeat x) = cons x (repeat x)

Note that:

• the code for repeat is exactly the same in the two cases,
• in each case the recursive call of repeat is found immediately below the constructor cons,
• in each case repeat produces a value of a coinductive record type,

and yet Agda accepts the first definition of repeat but rejects the second one (Termination checking failed for the following functions: repeat).

I'm aware that using the sized Thunk in the standard library the second version can be amended so that it is accepted by Agda. Nonetheless, I'd like to understand what makes the first version above so different from the second one that it passes the termination checker. They look basically the same to me.

Thanks!