[Agda] Big indices for small types?

[Conor McBride]

Hi folks

Just fiddling about with some ideas about stratification
and wondering if anyone has anything substantial to say
about definitions like

   data EQ (S : Set1) : Set1 -> Set where
     REFL : EQ S S

On the one hand, this doesn't exactly fit with the idea
of building the hierarchy up from below. On the other
hand, it doesn't actually store any big things inside
any small things.

Of course, Agda 2's

   data BEFORE : AFTER -> Set

distinction isn't the usual parameter/index distinction,
as shown

   data Lam (X : Set) : Set where
     var : X -> Lam X
     app : Lam X -> Lam X -> Lam X
     lam : Lam (Maybe X) -> Lam X

Sizewise, it seems that anything goes as long as there's
no large payload.

Is this well understood?

Scares me.

Cheers

Conor