>No compiler in existence makes these kinds of checks
If your claim is that no compiler in existence can make these kinds of checks at compile time, that's not true. Any dependently-typed language can do this (Idris, Coq, Agda, ATS). In fact, even a language with refinement types can do this, like Liquid Haskell.
And a number of languages do these checks at runtime: Ada and Nimrod are two that come to mind.
If your claim is that no compiler in existence can make these kinds of checks at compile time, that's not true. Any dependently-typed language can do this (Idris, Coq, Agda, ATS). In fact, even a language with refinement types can do this, like Liquid Haskell.
And a number of languages do these checks at runtime: Ada and Nimrod are two that come to mind.