You are, because the type still depends on the value of n. It's just that that value is unconstrained. It can still be used parametrically in type signatures, t

You are, because the type still depends on the value of n. It's just that that value is unconstrained. It can still be used parametrically in type signatures, though, e.g. append : Vect n a -> Vect m a -> Vect (n+m) a That's not possible without dependent types.