static exhaustiveness checking

[graydon]

Currently a non-exhaustive match is silently compiled and turns into a runtime fault if it hits the not-handled case. It'd be nice to at least have a warning, or perhaps strict checking, on non-exhaustive matches.

[rpearl]

This seems like a reasonable way learn my way around the rustc codebase. If I have a chance in the next week or so I'll look at this.

[catamorphism]

Taking this. If someone else is dying to do it, let me know...

[rpearl]

Yeah, I sadly don't have time for this, even though it looked interesting. Have fun.

[nikomatsakis]

I want this.

[catamorphism]

Working on it right now!

[catamorphism]

I have the code finished, which entailed making every non-exhaustive case in rustc and libraries exhaustive.

I won't check it in just yet because there were objections to it in a different issue discussion. With hope, we can discuss this tomorrow. My opinion: it's really important to be able to distinguish, immediately, between "I left out this case because I believe I can prove it's statically impossible to reach it" and "I forgot to include this case". If we don't have that, it's going to get really embarrassing. Just look at some of the experience reports from the darcs people about how many of the errors involved use of Maybe::fromJust (the Haskell equivalent of option::get) without proving that it wouldn't fail with a non-exhaustive match.

[catamorphism]

(also, when I was making alts exhaustive, it was almost never obvious to me why the omitted cases were unreachable. IMO, it's only excusable to omit cases if one either documents why, if the invariant that makes it safe is so obvious that someone can tell from glancing at the code that it's true.)

[kud1ing]

"I left out this case because I believe I can prove it's statically impossible to reach it":

I think "impossible" situations could be documented with an assertion and an explanation quite nicely like: _ { assert(false); } // will never happen, because XYZ

[catamorphism]

@Lenny222 That's at least the minimum we could strive for, again IMO. Ideally, the type system will eventually be precise enough that we can get rid of all but a few of "assert(false)"s. (Hopefully at least a 'fail "helpful message"' instead of assert(false).)

[kud1ing]

Agreed.

[catamorphism]

Fixed in fba35e1 -- also see #1679 for some discussion of features that could help reduce the need for redundant cases. In the meeting today, we also discussed using attributes to mark particular alt expressions as non-exhaustive, but that's for future work.