[Agda] This ain't right, is it?

[Benja Fallenstein]

Hi all,

The following type-checks with the darcs version of Agda (and
--universe-polymorphism):

IsThatRight : {i : Level} → Set i
IsThatRight {i} = (R : Set i) → R

Isn't that like set-in-set? Agda does object to this:

That'sNotRight : Set
That'sNotRight = (R : Set) → R

Thanks,
- Benja