Dependent types can do this. This is information that can be known at compile time by means of a proof that the values are what they should be (or within certain bounds) through the entire call chain.