Therefore, there cannot possibly be a way to avoid the problem I described in my example, unless your program exists in a a closed world where there are no inputs, and the values of all variables are defined before compilation.
The word "total" invokes the totality checker[0] which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven to not enter an infinite loop.
(Also, bear in mind languages like Haskell use "lazy" or "non-strict" evaluation by default, where values aren't evaluated until they're actually needed; kiiiinda like Streams?)
I'm certainly not an expert on Idris, but I imagine dependent typing provides two benefits:
1) The type signature (which is separate from the implementation; kind of like an Interface in Java) can enforce constraints on your implementation. So, if you define a function with type sig of "Int a => Int b => (a + b)", your implementation must ensure that the returned value is equal to the sum of the two inputs.
2) You can look purely at the type signature to understand what a function is doing. Looking at that type signature above, I can see I want to use that function for addition, not multiplication.
Anyway, I'm absolutely not doing justice to these ideas (mostly because I'm not well acquainted with the languages). If you're curious at all, I would highly recommend taking a course on functional programming as a minimum; once I realised that names are meaningless in code, you start seeing everything as reducible to very similar type signatures, which makes you yearn for a language that lets you write your boilerplate once, in a polymorphic way (beyond generics).
That would make many practical, real-world programs noncompilable. Any program which accepts data via API calls, or even reads strings from STDIN, cannot know what values are going to be passed to it before it runs. Compilers cannot predict the future.
This statement is false. I recommend reading about dependent types, which enable exactly what you claim is impossible.
It's true that in every mainstream language, the type system is not powerful enough to reason about types that "depend" on values, such as the type of MxN matrices, sorted lists, prime numbers, etc. But don't limit your sense of what is possible by your experience with mainstream languages; most have rather limited type systems compared to what we know is possible in theory.
That is a true statement for any program that accepts input, strictly speaking. The halting problem is unsolvable.
The halting problem cannot be solved in general, but some programs can be proven to halt (or not halt). That's how the first few Busy Beaver numbers were found.
For something more substantial: a correct program that implements a regular language recognizer will always halt eventually on any input, because it always makes progress and doesn't have any nonterminating loops. It consumes the whole input and stops.
The hard part is proving you wrote it correctly, but that's what coq et al are for.
Analogous statements are true for programming in a dependently typed language.