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?