[GHC] #15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints

[GHC]

#15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under
unsatisfiable constraints
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12957            |  Differential Rev(s):  Phab:D5017
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Be careful. You're conflating two separate issues:

 1. Should we emit coverage warnings in unreachable alternatives?
 2. Should `EmptyCase`'s code path (`checkEmptyCase'`) behave differently
 than other `case` expressions' code path (`checkMatches'`)?

 I don't feel strongly about (1), and I think we could just as well answer
 that question with "yes" or "no". Matthew, can you comment here? You're
 the one who introduced this convention.

 The answer to (2) is an emphatic "yes". If you try to delete
 `checkEmptyCase'`, then //all// `EmptyCase` expressions will be reported
 as non-exhaustive (this isn't just speculation on my part; I actually
 tried this). And this is not surprising. Regular `case` expressions are
 lazy, whereas `EmptyCase` expressions are strict. Hypothetically speaking,
 if `EmptyCase` were lazy, then in the following code:

 {{{#!hs
 data Void

 absurd :: Void -> a
 absurd x = case x of {}

 main :: IO ()
 main = putStrLn (absurd undefined)
 }}}

 `main` would produce a non-exhaustive pattern-match error at runtime
 instead of an `undefined` exception! This alone shows that `EmptyCase`
 needs some degree of special-casing.

 While an interesting discussion, (2) doesn't pertain much to this ticket,
 so I'd encourage you not to bog down the discussion with mention of it.
 (Feel free to open a separate ticket if it's bothering you that much.)

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