Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints

Consider the following code:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

f :: (Int ~ Bool) => Bool -> a
f x = case x of {}

g :: (Int ~ Bool) => Bool -> a
g x = case x of True -> undefined

$ /opt/ghc/8.4.3/bin/ghci Bug.hs
GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:10:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: False
   |
10 | g x = case x of True -> undefined
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Observe that we get a non-exhaustivity warning for the case expression in g (thanks to commit adb565aa), but not for the one in f. The difference is that f uses EmptyCase, whereas g does not, and the codepath for EmptyCase is unfortunately incongruous with the codepath for other coverage checking.

I know how to fix this. Patch incoming.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture