[GHC] #15385: -Wincomplete-patterns gets confused when combining GADTs and pattern guards

[GHC]

#15385: -Wincomplete-patterns gets confused when combining GADTs and pattern guards
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternMatchWarnings               |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following code:

 {{{#!hs
 {-# 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.

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