story
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.
In dependently typed programming languages like agda and Idris typechecking is decidable. You are wrong here.
Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.
There's a reason dependent types haven't caught on in industry, and even the "fancy" types that are cited by proponents as being used in practice (like ML's Hindley-Milner type system) are MUCH simpler than full blown dependent type systems. Because the burden is shifted to the programmer, and that makes it super unusable.
I'm not a dependent types hater. (I have dependent type friends :) ). But the best way to get a usable type system is to restrict it's expressivity to make automation easier, and the annotation burden much smaller. Sure, we're giving up something there. But it's better than having a system that can prove any theorem in the Calculus of Constructions, but used by about thirty people.
That's why we need gradual typing. Some critical parts should be written with full dependent types with termination checker, etc, but most of the code should be just type checked.
P.S. I have some dependent types experience, including applying Coq in commercial projects.
A loose reading (probably overly loose, but possibly what was intended rather than what was expressed) would permit something closer to "Dependent types, in full generality, are undecidable to type check." which I believe to be the case, where actual implementations are more constrained (though decreasingly so!).
