To elaborate a bit further, the reason that the original isn't exhaustive is that to know that, you would have to execute arbitrary code at compile time, the 'if'. The exhaustiveness check is only on the `y` part of the pattern.
I mean, if you only match on the integer value, this case is trivial. Similar cases are already analysed by gcc to tell you "this comparison is always true/false".
I know it doesn't generalise and it "is it worth doing" may be a question, but it seems like most match blocks would fall easily under a very limited set of known cases.
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).
