There are "provers not based on type theory", most notably the Mizar system, that still prefer types (where possible) to propositions and proof obligations. Mostly, because type checking and type inference are inherently a lot more efficient than fully-general proof checking and automated proving - hence it's convenient to have a separate formalism for the efficient subset of logic that's restricted to such "taxonomy-like" reasoning. (There is a similar case for using restricted "modalities" instead of fully-general first order logic for reasoning over "possible worlds": that too involves a significant gain in efficiency.)

(And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)