This is a feature some (experimental) programming languages have - look into dependent types. The long-and-short of it is that it adds a lot of power, but comes at an ergonomic cost - the more your types say about your code, the more the type checker needs to be able to understand and reason about your code, and you start to run up against some fundamental limits of computation unless you start making trade-offs: giving up Turing-completeness, writing proofs for the type checker, stuff like that.
Another interesting point of reference are "refinement types", which allow you to specify things like ranges to "refine" a type; the various constraints are then run through a kind of automated reasoning system called an SMT solver to ensure they're all compatible with each other.
Another interesting point of reference are "refinement types", which allow you to specify things like ranges to "refine" a type; the various constraints are then run through a kind of automated reasoning system called an SMT solver to ensure they're all compatible with each other.