Erased arguments in type constructors

Question

What does it mean to erase an argument in a type constructor? For example

data Foo : (0 _ : Nat) -> Type where

as opposed to

data Foo : Nat -> Type where

My understanding is that nothing in a type constructor is used at runtime anyway, so it's effectively always 0. I guess it also leads to the perhaps more confusing question of what would a linear argument mean in a type constructor, but that's for another day.

Answer 1

Idris (2) is somewhat unusual in that it allows direct pattern matching on types. Type constructors are treated as Type's constructors.

finSize : Type -> Maybe Nat
finSize (Fin n) = Just n
finSize _       = Nothing

If you, say, erased Fin's argument, then matching against a Type with Fin n would make n erased, too.

data Fin : (0 _ : Nat) -> Type where

-- fails
-- finSize : Type -> Maybe Nat
-- finSize (Fin n) = Just n  -- have 0 copies of n, need at least 1
-- finSize _       = Nothing
-- succeeds
data Erased : Type -> Type where Erase : (0 _ : a) -> Erased a
finSize : Type -> Maybe (Erased Nat)
finSize (Fin n) = Just (Erase n)
finSize _       = Nothing