open import Agda.Builtin.Nat

data The {ℓ}{A : Set ℓ} : A → Set ℓ where
  the : (a : A) → The a

_ : The 
_ = the 

toNat : ∀ {n : Nat} → The n → Nat
toNat {n} _ = n

test : Nat
test = toNat (the )
{-# COMPILE AGDA2LAMBOX test #-}