Tool for checking the safety of non-exhaustive patterns

[catamorphism]

This is definitely in the department of blue-sky, out-there projects, but I was just thinking about option::get and wondering how feasible it would be to adapt the ideas in Neil Mitchell's Catch tool (for Haskell) to Rust.

http://community.haskell.org/~ndm/catch/

In our case, this would be to verify that alt check, and maybe even functions that pattern-match on their input and unconditionally fail in one or more branches (like option::get) are being used safely (which is to say, in a way that won't cause a runtime failure). This would be one way to allow alt checks and get a safety guarantee.

Mutability would definitely complicate things, but one way out is to only provide any guarantees about immutable data (and warn in a lint pass about alt check and similar things on mutable data).

[catamorphism]

(Of course, we might just get rid of alt check... but we'll always have option::get, probably. This certainly isn't necessary, but in case someone who likes static analysis wanted to pick it up for fun...)

[pnkfelix]

Nominating for milestone: far future.

[pnkfelix]

accepted for far future

[thestinger]

Triage bump.

[emberian]

Visiting for triage. alt check is now known a match.

[pnkfelix]

I think we should close this ticket at this point; the language has changed quite a bit since it was written so that it is hard for an average community member to actually know what it is really asking for.

(I suppose now that we have the ability to put attributes on match arms, it would be feasible to annotate match arms, where the attribute would indicate whether we want the hypothetical tool to warn about whether they are actually reachable. But still, I think we should close this; tools like this can be added in the future, but it need not be a task that the rust team undertakes, and it does not require changes to the language nor core tools.)

@pnkfelix Agreed. Regardless of how feasible a Rust version of Check is, it seems out of scope of the compiler. Could this be closed?