-Wincomplete-patterns gets confused when combining GADTs and pattern guards

Consider the following code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

import Data.Kind

data family Sing :: forall k. k -> Type
newtype Id a = MkId a
data So :: Bool -> Type where
  Oh :: So True

data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True
data instance Sing :: Ordering -> Type where
  SLT :: Sing LT
  SEQ :: Sing EQ
  SGT :: Sing GT
data instance Sing :: forall a. Id a -> Type where
  SMkId :: Sing x -> Sing (MkId x)

class POrd a where
  type (x :: a) `Compare` (y :: a) :: Ordering

class SOrd a where
  sCompare :: forall (x :: a) (y :: a).
              Sing x -> Sing y -> Sing (x `Compare` y)

type family (x :: a) <= (y :: a) :: Bool where
  x <= y = LeqCase (x `Compare` y)
type family LeqCase (o :: Ordering) :: Bool where
  LeqCase LT = True
  LeqCase EQ = True
  LeqCase GT = False

(%<=) :: forall a (x :: a) (y :: a). SOrd a
      => Sing x -> Sing y -> Sing (x <= y)
sx %<= sy =
  case sx `sCompare` sy of
    SLT -> STrue
    SEQ -> STrue
    SGT -> SFalse

class (POrd a, SOrd a) => VOrd a where
  leqReflexive :: forall (x :: a). Sing x -> So (x <= x)

instance POrd a => POrd (Id a) where
  type MkId x `Compare` MkId y = x `Compare` y

instance SOrd a => SOrd (Id a) where
  SMkId sx `sCompare` SMkId sy = sx `sCompare` sy

-----

instance VOrd a => VOrd (Id a) where
  leqReflexive (SMkId sa)
    | Oh <- leqReflexive sa
    = case sa `sCompare` sa of
        SLT -> Oh
        SEQ -> Oh
        -- SGT -> undefined

What exactly this code does isn't terribly important. The important bit is that last instance (VOrd (Id a)). That //should// be total, but GHC disagrees:

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

Bug.hs:63:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: SGT
   |
63 |     = case sa `sCompare` sa of
   |       ^^^^^^^^^^^^^^^^^^^^^^^^...

As evidence that this warning is bogus, if you uncomment the last line, then GHC correctly observes that that line is inaccessible:

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

Bug.hs:66:9: warning: [-Winaccessible-code]
    • Couldn't match type ‘'True’ with ‘'False’
      Inaccessible code in
        a pattern with constructor: SGT :: Sing 'GT, in a case alternative
    • In the pattern: SGT
      In a case alternative: SGT -> undefined
      In the expression:
        case sa `sCompare` sa of
          SLT -> Oh
          SEQ -> Oh
          SGT -> undefined
   |
66 |         SGT -> undefined
   |         ^^^

Clearly, something is afoot in the coverage checker.

Trac metadata

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