This is my understanding of what dependent types [1] will allow you to accomplish (at least in some imaginary future).

[1] https://en.wikipedia.org/wiki/Dependent_type