What you're talking about is dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type). The problem with these

What you're talking about is dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type). The problem with these is that, in general, determining whether or not an object is of one of these types (PositiveNumber, PrimeNumber, ListWithAtLeastThreeElements, etc.) at compile time is undecidable. This isn't horrible, as template meta-programming already allows you to encode Turing Complete programs into compilation, but unlike templates, where evaluation is somewhat straightforward, evaluating dependent types requires general theorem proving. There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete.