I don't understand this sentence.
Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to occasionally run Idris functions (that's what makes it dependent). This is in fact the only source of potential non-termination in the checker. So, whenever Idris needs to run a function compile time, and it cannot prove termination via the checker, it just throws an error.
(Side note: it is never required to run a function in order to the typecheck the very same function. All major dependent type checkers has the property that they never have to run a function that is not already checked).
All of this is certainly the case, and useful, and interesting. It doesn't contradict the point that 1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible, which was approximately the original question.
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".
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.