> "Runtime value" is an implementation detail. You could write an Idris interpreter. Sure. And such an interpreter would still not interpret types at runtime,

> "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.)