A dependent type system needn't be able to express that a type is indexed by an even number. You can have dependent types without type-level computation, for ex

A dependent type system needn't be able to express that a type is indexed by an even number. You can have dependent types without type-level computation, for example, by requiring that types be parameterized by nonexpansive expressions - which is nevertheless already more powerful than what Haskell's type system offers. This restriction might even be a good thing for type inference.