Yes, it is possible for some cases—this is dependent types' bread and butter—but having an analysis in the type system that sometimes falls down in complex cases tends to lead to frustrating type errors, because it'll refer to types and constraints that the you didn't type and the compiler inferred. If we really wanted to go down this road, we would probably want to add real dependent types to Rust and surface them in the type grammar. (I personally think Rust 1.0 has spent its complexity budget, though, and I'd rather have HKT first in any case.)
It's the same reason why we don't adopt a Nim-like "disjointness analysis" that can reason about arithmetic (as mentioned in the article).
It's the same reason why we don't adopt a Nim-like "disjointness analysis" that can reason about arithmetic (as mentioned in the article).