-- {-# OPTIONS --level-universe #-}
open import Agda.Builtin.Nat using (Nat; suc)

open import Agda.Primitive

-- ** level definitions should be ignored
0ℓ : Level
0ℓ = lzero

mkLevel : Nat → Level
mkLevel  = 0ℓ
mkLevel (suc n) = lsuc (mkLevel n)

-- ** level function arguments should be erased
testLevel : Level → Nat
testLevel _ = 

-- ** level application arguments should be erased
testMkLevel : Nat
testMkLevel = testLevel (mkLevel )

-- ** level record fields should be erased
record SomeLvl : Set where
  constructor this
  field ℓ : Level
open SomeLvl public

someLvl : SomeLvl
someLvl = this 0ℓ

lvlToNat : Level → Nat
lvlToNat _ = 

testSomeLvl : Nat
testSomeLvl = lvlToNat (someLvl .ℓ)

constLvl : ∀ {A : Set} → A → Level → A
constLvl x _ = x

testConstLvl : Nat
testConstLvl = constLvl  (someLvl .ℓ)

const : ∀ {A B : Set} → A → B → A
const x _ = x

testConst : Nat
testConst = const  

testConstLvl2 : Nat
testConstLvl2 = const  (someLvl .ℓ)

testWhere : Nat
testWhere = toNat (someLvl .ℓ)
  where
  toNat : Level → Nat
  toNat _ = 

open import Agda.Builtin.Nat

test : Nat
test = testMkLevel + testSomeLvl
     + testConst + testConstLvl2 + testWhere
{-# COMPILE AGDA2LAMBOX test #-}