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.
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