You do not even need to use dependent types. You could just restrict yourself to polymorphic types if you wanted to. And you could use dependent types just for the things that don't require any "proving" work. Returning multiple types from a function, implementing type-safe `printf`, checking out-of-bound errors at compile time, things like that.

Dependent types allow you to express things such as `a == b` as a type, and proving that requires some work, but you don't need any of that at all. Idris is a superset of Haskell, you may say.