Recursion through delayed evalution impossible?

 So, I want to do something in agda, consider the following type:

data Genlist (A : Set) : Set where
  cons : A -> Genlist A -> Genlist A
  generator : ((tt : ⊤) -> Genlist A) -> Genlist A

The type captures the notion of finite but expandable lists. But because agda doesn't understand that delaying a computation can guarantee termination I need to bypass the type checker with a pragma.

  {-# TERMINATING #-}

  ones : Genlist Nat

  ones = generator (\x -> cons 1 ones)

Unfortunately, that also comes with the following cost. You can prove that the type isn't inhabited.

  data ⊥ : Set where

  uhh : ∀ {A} → Genlist A → ⊥

  uhh (cons _ x)    = uhh x

  uhh (generator x) = uhh (x tt)

The type system needed would, apart from allowing recursion with delayed computation, also need to keep track of how often you force a computation.