[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 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??

 What about simpler cases
 {{{
 data T a where
   T1 :: T Int
   T2 :: T a

 f :: T Bool -> Int
 f T1 = ....(case x of { True -> False })...
 f T2 = ...
 }}}
 The entire RHS of the first equation is unreachable.  Should we not just
 stop reporting errors from that branch altogether?   If the door wasn't
 shut (say we had learned something about `x`, but nothing contradictory)
 then the inner case might be fine.  The more we learn about `x` the fewer
 alternatives we may need in that inner case.

 When the door shuts altogether we need no branches in the inner case, so
 perhaps reporting a redundant match is correct.  Or perhaps we just want
 to shut up once we find a contradiction, and let the user fix that first.
 But discarding all the constraints seems ... unexpected.

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