Lint should check for inexhaustive alternatives

GHC's simplifier prunes inaccessible alternatives from case expressions. E.g.

case x of
  A y -> e1
  _   -> ....(case x of
                A y -> r1
                B -> r2
                C -> r3) ...

It'll prune the A alternative from the inner case to get

case x of
  A y -> e1
  _   -> ....(case x of
                B -> r2
                C -> r3) ...

BUT, there is no independent check from Lint that this pruning does the Right Thing. Yet, lacking such a check, a program can pass Lint and then seg-fault, which is Very Bad.

Trac #11172 (closed) is an example. It turned out to be a bug in the pruning, which led to something like

case x of
  Left y -> e1

but in fact x ended up being bound to (Right v) for some value v. But because there is only a single alternative left, GHC does not test the tag, but instead goes ahead and accesses it the Right value as if it was a Left value. And because of pointer-tagging, it'll assume the wrong tag on the pointer, and very soon you are in seg-fault land.

So this ticket is to suggest: make Core Lint do it's best to check that all cases are in fact exhaustive. There are two ways in which we prune cases:

• Enclosing pattern matches (as above)
• GADT pattern matches may be exhaustive even when they don't mention all constructors.

For the latter, it's impossible for Lint to reproduce all the reasoning of the type checker, but I bet that in 99.5% of the cases the existing function dataConCantMatch will do the job.

So if Lit

• Maintains an environment saying what each variable can't match (as the simplifier does)
• Does a simple-minded dataConCantMatch test based on the typ of the scrutinee

I think we'd be a long way forward. It's possible that a valid program could trigger a Lint report, but let's see.

Any volunteers?