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

[effectfully]

Hi. I have a data type that contains a lot of level arithmetic. In
order to satisfy the typechecker I have to write

  call   : ∀ {Rs Rs′} i
         -> (Lift∃ᵐ (lsuc ∘ proj₁) i αεs λ A ->
               Lift∃ᶻ r′ˡ i αεs ρs λ R′ ->
                 Lift∃ᵐ proj₂ i αεs {lookupᶻ i Ψs (lookupᵐ i Rs) A R′} λ _ ->
                   Lift∀ᵐ  proj₁ i αεs λ x ->
                     Eff Ψs B (replaceᵐ i (R′ x) Rs) Rs′)
         -> Eff Ψs B Rs Rs′

instead of

  call   : ∀ {Rs Rs′} i {A R′}
         -> lookupᶻ i Ψs (lookupᵐ i Rs) A R′
         -> (∀ x -> Eff Ψs B (replaceᵐ i (R′ x) Rs) Rs′)
         -> Eff Ψs B Rs Rs′

Those `Lift*' are functions, so I'm no longer able to write

  h (call i a f) = ...

Instead, it's

  h (call i p) = let a , f = runLifts p in ...

(I haven't tried yet to define this `runLifts' though).

It would be great to have something like a NO_UNIVERSE_CHECK pragma,
so it's possible to write e.g.

{-# NO_UNIVERSE_CHECK #-}
data D α β : Set β where
  c : Set α -> D α β

Is is possible to implement or somehow emulate this in Agda?