Type indices and runtime erasure

Stream: general

[Phil Nguyen]

For a type such as the textbook definition of lists that track lengths, is the length n always retained at runtime, or only when it's ever used in runtime code? Is there a way to check if an index is retained at runtime without inadvertently causing it to be retained? A related question: Is there a way to mark an index as "not wanted at runtime" so it can't accidentally be retained? Thanks!

inductive Vect (t : Type) : Nat → Type where
| nil : Vect t 0
| cons : t → Vect t n → Vect t (n + 1)

def Vect.size : Vect t n → Nat
| _ => n

def xs := Vect.cons "foo" $ Vect.cons "bar" $ Vect.nil
#eval xs.size