[JadeNB]

Without really addressing your question, notice that the power of dependently typed languages is not in the intelligence of the compiler, but in the expressivity of the type system. That is, the question becomes not "can the compiler catch this error on its own?", but rather "can the compiler verify my proof that I have not made this error?" A language with a very powerful type system can still have a very dumb compiler (although it will generate extremely slow code).

EDIT: It occurs to me that this is well summarised by the apparently facetious remark "Ask not what your compiler can do for you; ask what you can do for your compiler."