[Agda] Strictly positivity of indexed families

[Florent Balestrieri]

Hello, I'd like to know if there is a workaround for  defining the 
following datatype which is rejected by the termination checker although 
it seems reasonable to me.  If there is a theoretical argument to rule 
out such definitions, I would welcome your explanations.

-- This datatype is rejected by agda.

data D : Nat -> Set where
  z : {n : Nat} -> D n
  s : {n : Nat} -> (D n -> Nat) -> D (suc n)

-- But we can expand the family as much as we want
-- without getting into trouble.

data D0 : Set where
  z : D0

data D1 : Set where
  z : D1
  s : (D0 -> Nat) -> D1

data D2 : Set where
  z : D2
  s : (D1 -> Nat) -> D2

data D3 : Set where
  z : D3
  s : (D2 -> Nat) -> D3


-- Florent