[GHC] #10746: No non-exhaustive pattern match warning given for empty case analysis

[GHC]

#10746: No non-exhaustive pattern match warning given for empty case analysis
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #7669, #11806     |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by gkaracha):

 Replying to [comment:16 dfeuer]:
 > {{{#!hs
 > Prelude> :set -XEmptyCase -XEmptyDataDecls
 > Prelude> data Void
 > Prelude> let absurd :: Void -> a; absurd x = case x of
 > Prelude> absurd (error "Really?")
 > *** Exception: Really?
 > }}}

 Wow! I was indeed not familiar with this unintuitive design choice, you
 are right.

 Replying to [comment:17 dfeuer]:
 > To summarize, empty case is desugared specially. It therefore needs a
 special case for coverage checking, but ''not'' the trivial one we
 currently have. I suspect the right thing is probably to avoid including
 `_|_` in `mkInitialUncovered` when checking an empty `case`, whatever that
 involves. You may need to do something else if you want to catch an
 overlapping trivial pattern in since cases, but even if you miss that it's
 no big deal.

 Overlap checking is not affected by this I think. Since this eager
 evaluation happens only in the `EmptyCase` case, there are no patterns to
 be considered redundant. Nevertheless, the case needs special treatment.
 The best fix I can think about this is a function
 {{{#!hs
 areInhabited :: [Id] -> TcM [ValVec]
 }}}
 which unfolds everything to WHNF if possible (recursively, I guess, if
 there are strict fields) and checks for satisfiability (approximately, of
 course, since this may not terminate). Then, `checkMatches'` could be
 adjusted:
 {{{#!hs
 checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
 checkMatches' vars matches
   | null matches = areInhabited vars >>= \us -> return ([],us,[])
   | otherwise    = ...
 }}}
 Does this sound reasonable? I'd like to think this through first, but I
 could write such a fix.

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