[GHC] #2431: Allow empty case analysis (was: allow empty case analysis)

[GHC]

#2431: Allow empty case analysis
------------------------------------+---------------------------------------
    Reporter:  RalfHinze            |       Owner:                  
        Type:  feature request      |      Status:  new             
    Priority:  low                  |   Milestone:  _|_             
   Component:  Compiler             |     Version:  6.8.3           
    Keywords:  empty case analysis  |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple     |     Failure:  None/Unknown    
  Difficulty:  Unknown              |    Testcase:                  
   Blockedby:                       |    Blocking:                  
     Related:                       |  
------------------------------------+---------------------------------------

Comment(by simonpj):

 I didn't find the above entirely clear, so Richard elaborates: consider:
 {{{
 data a :~: b where
   Refl :: a :~: a

 absurd :: True :~: False -> a
 }}}
 Now, I want to write a term binding for `absurd`. Here are two candidates:
 {{{
 absurd x = error "absurd"    -- (A)
 absurd x = case x of {}      -- (B)
 }}}
 I much prefer (B). Why?  Because GHC can figure out that `(True :~:
 False)` is an empty type. So (B) has no partiality and, (if #3927 is
 fixed) I should be able to compile with `-fwarn-incomplete-patterns` and
 `-Werror`.

 On the other hand (A) looks dangerous, and GHC doesn't check to make sure
 that, in fact, the function can never get called.

 The bottom line, for me at least, is that I want to avoid the partial
 constructs (incomplete patterns, undefined, etc) in Haskell as much as
 possible, especially when I'm leveraging the type system to a high degree.
 The lack of empty case statements forces me to use undefined where it
 isn't really necessary.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2431#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler