[GHC] #11475: Lint should check for inexhaustive alternatives

21 Jan 2016

      #11475: Lint should check for inexhaustive alternatives
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.  Trac #11172 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?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11475
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler