> Other than an Ada example, or dependently-typed languages that aren't use in production...
Every time someone gives you an answer, you modify the question to exclude it. Eventually you will have excluded everything that refutes the fallacy in your original post, but it is still there.
Such subsets are readily available in all dynamic languages I've used. But the issue here is really about compile-time checking these things, and that's a different animal.
Ok, how? Other than an Ada example, or dependently-typed languages that aren't use in production, can you offer an example?