Re: [GHC] #13990: Core Lint error on empty case

20 Jul 2017

      #13990: Core Lint error on empty case
-------------------------------------+-------------------------------------
        Reporter:  mbieleck          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.2.2
       Component:  Compiler          |              Version:  8.2.1-rc3
      Resolution:                    |             Keywords:  core-lint
                                     |  case
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Hmm.

 Let's stand back a bit.

 * The simplifier (via `CoreSyn.filterAlts`) can eliminate branches of a
 case that can't happen, because of (a) GADT matching and (b) lexically
 enclosing case expressions.

 * Lint can't guarantee to come to the same conclusion becuase of floating.
 Eg
 {{{
 data T = A | B | C

 f x = case x of
         A -> e1
         _ -> ...(case x of
                    B -> e1
                    C -> e3)...
 ===>
 f x = let t = case x of
                    B -> e1
                    C -> e3
       in case x of
            A -> e1
            _ -> ...t...
 }}}
   Before, it's clear that the inner case is exhaustive, but not so clear
 after the transformation.

 * So currently Lint doesn't attempt to complain about inexhaustive cases.

 * EXCEPT if there are zero alternatives.  And for that, strangely, Lint
 makes two separate checks.  First, in the `Case` equation for
 `lintCoreExpr`:
 {{{
      -- See Note [No alternatives lint check]
      ; when (null alts) $
      do { checkL (not (exprIsHNF scrut))
           (text "No alternatives for a case scrutinee in head-normal
 form:" <+> ppr scrut)
         ; checkWarnL scrut_diverges
           (text "No alternatives for a case scrutinee not known to diverge
 for sure:" <+> ppr scrut)
         }
 }}}
   Second in `checkCaseAlts`:
 {{{
      ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
               (nonExhaustiveAltsMsg e) }
 }}}
   Clearly we should do this stuff in only one place.

 I now propose that we remove the "null alts" check altogether.  It's just
 an extreme case of having filtered out all alternatives.  The current code
 treats it specially, but this ticket has convinced me that it's not
 special afte all.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:9
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler