[Agda] Strictly positive

[Kenichi Asai]

I am trying to encode in Agda the two-level types as introduced by
Sheard and Pasalic [1].  For example, I can encode the type for simple
types as follows:

----------------------------------
module main where

data t (Type : Set) : Set where
  TInt : t Type
  TArrow : Type -> Type -> t Type

data fix : Set where
  Fix : t fix -> fix
----------------------------------

where the parameter "Type" for t shows where the recursion occurs
(i.e., the two arguments of TArrow).  Now, I want to generalize t
to an arbitrary type (so that it can be given by users later).  I
considered:

----------------------------------
module Test (t : Set -> Set) where

data fix : Set where
  Fix : t fix -> fix
----------------------------------

but Agda complains:

> fix is not strictly positive, because it occurs in an argument to a
> bound variable in the type of the constructor Fix in the definition
> of fix.

Sure, if I instantiate t to:

t : Set -> Set
t Type = Type -> Type

it does lead to inconsistency.  But my intention is that I instantiate
t always as something that is strictly positive in its argument (like
the t for simple types above).  Is there any way to declare so, so
that fix can be defined independently of the definition of t?

Thank you in advance.

Sincerely,

[1] Tim Sheard and Emir Pasalic
"Two-level types and parameterized modules"
Journal of Functional Programming, 14(5):547-587, September 2004.

-- 
Kenichi Asai