That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker.
At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
> "Runtime value" is an implementation detail. You could write an Idris interpreter.
Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values.
Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types.
> It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?
Whether that would be anyhow "useful" depends on the definition of "file usage".
If there's any reference form the "used" parts of the program to the "unused file" you have a problem:
A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless.
(Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)
