[Agda] Positivity checker

[Wouter Swierstra]

When I define the following data type in Agda, the positivity checker  
complains:

data Data : Nat -> Set where
   Base : Data Zero
   Step : forall {n} -> (Data n -> Data n) -> Data (Succ n)

This declaration reeks of negativity, but on closer inspection it  
shouldn't really be a problem. The index limits the amount of  
recursion that can be done. You run into problems immediately if you  
try to do things like:

app : forall {n} -> Data n -> Data n -> Data n
app (Constructor f) x = f x

omega : forall {n} -> Data (Succ n)
omega = Constructor (\d -> app ? d)

The indexing prevents the usual "self-application" from type checking.

I suppose I could define a function into Set instead of a data type,  
but I'd much rather work with data (the example I have in mind is  
pretty complicated).

Is there a way to define this kind of data type without switching off  
the positivity checker? Thanks,

   Wouter