[Agda] Is it possible to switch off universes checking?

[Nils Anders Danielsson]

On 2015-12-28 18:55, effectfully wrote:
> {-# NO_UNIVERSE_CHECK #-}
> data D α β : Set β where
>    c : Set α -> D α β
>
> Is is possible to implement or somehow emulate this in Agda?

Let's try. First attempt:

   {-# OPTIONS --type-in-type #-}

   data D α β : Set β where
      c : Set α -> D α β

Result:

   Use --universe-polymorphism to enable level arguments to Set
   when checking that the expression Set β is a type

Second attempt:

   {-# OPTIONS --type-in-type --universe-polymorphism #-}

   data D α β : Set β where
      c : Set α -> D α β

Result:

   Cannot have both universe polymorphism and type in type.

I don't know why universe polymorphism and --type-in-type cannot be used
together.

-- 
/NAD