[Someone]

"1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible"

You do need more bandwidth. Trivial counterexample (for any reasonable inference of the semantics of the source code of this made-up language):

  define isCorrectlyTyped( program P)
  as
    return "no".

Of course, a practical version would have to have the function return "yes" on more valid programs :-)

By the way: compilers for languages such as Java and C# do something similar: they reject all programs that may use a variable before a value is assigned to it, at the price of rejecting some programs that properly assign a value to each variable before use on the grounds that the compiler cannot prove it. Typically, the language specification describes exactly how smart compilers can be (or rather, how stupid compilers must be) when checking this, to ensure that all compilers agree about what programs are valid.

[dllthomas]

Fair point! I was wrong above - "Can a dependent type system catch all type errors at compile time?" Yes, so long as you're okay with rejecting some correctly typed programs! If you're not okay with that, then your type checker might not halt. Shame it's too late to add an addendum above...