[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:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: mpickering (added)


Comment:

 Replying to [comment:2 simonpj]:
 > (Commenting here because my reflections concern the specification, not
 the coding.)
 >
 > The patch says
 > {{{
 > We decide to better than this. When beginning coverage checking, we
 first
 > check if the constraints in scope are unsatisfiable, and if so, we start
 > afresh with an empty set of constraints. This way, we'll get the
 warnings
 > we expect.
 > }}}
 > That seems quite odd behaviour!   The door closes gradually, but when it
 becomes shut we slam it open again??

 This is all explained in the commentary in
 https://phabricator.haskell.org/D3064 (which I've attempted to turn into
 Note form in this patch). Also cc'ing mpickering, who established this
 convention.

 Replying to [comment:3 simonpj]:
 > Another thing.  I see in `Note [Checking EmptyCase Expressions]` (in
 `Check.hs`) this:
 > {{{
 > Empty case expressions are strict on the scrutinee. That is, `case x of
 {}`
 > will force argument `x`. Hence, `checkMatches` is not sufficient for
 checking
 > empty cases, because it assumes that the match is not strict (which is
 true
 > for all other cases, apart from EmptyCase). This gave rise to #10746.
 > }}}
 > I had no idea!  The [http://downloads.haskell.org/~ghc/master/users-
 guide/glasgow_exts.html#empty-case-alternatives user manual entry] says
 nothing about this non-uniform behaviour of empty case expressions.
 >
 > What actually stops us from treating an empty case as an ordinary case
 expression with no alternatives?  Anything else seems.. unexpected.

 I'm not sure I understand this question. Did you read #10746? That seems
 to lay out pretty clearly why `EmptyCase` needs to be treated specially
 (because it's strict, unlike other `case` expressions).

 > The explanation in the user manual is cryptic (see the text about
 `absurd`.  And it relates directly to this ticket, because it has `True ~
 False` in scope, which is a contradiction.  So maybe fixing comment:2
 would mean we could treat case expressions uniformly, which would mean we
 could delete code?

 Maybe. But I have no interest in doing this here. I only opened this
 ticket because the lack of sharing between code paths in `checkEmptyCase`
 and `checkSingle` made it difficult to implement #15305, so I did the
 exact minimum amount of work to fix the discrepancy. Anything more than
 this deserves to be in a separate feature request, in my opinion.

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