Obtaining a value that was supposed to be erased at run time

Consider the following dependent data type definition:

data Container : Nat -> Type where
   Level : {n : _} -> Container n

The following function compiles:

getLevel : Container n -> Nat
getLevel Level = n

However, if I specify a multiplicity of zero instead of unrestricted for n in Level:

data Container : Nat -> Type where
   Level : { 0 n : _ } -> Container n
            ^^^

Then, the function getLevel no longer compiles:

Error: While processing right hand side of getLevel. n is not accessible in this context.

This makes sense to me because the zero multiplicity means that n is erased at run time. However, if I write getLevel type as:

getLevel : {n : _} -> Container n -> Nat

getLevel does compile. I'm aware of {n : _} implying unrestricted multiplicity for n. What I don't understand is how this can possibly work since n in Level has already been erased at run time and that is what is used to create a Container n value.

getLevel : {n : _} -> Container n -> Nat
getLevel Level = n

Here n is an implicit argument with unrestricted multiplicity to getLevel, which is returned. It compiles for the same reason the following code does.

getLevel : {n : Nat} -> Nat
getLevel = n