-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

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import labels

Actually, this is even simpler than I made it out to be:

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

import Data.Type.Equality

data T a where
  TInt  :: T Int
  TBool :: T Bool

f :: a :~: Int -> T a -> ()
f eq t
  | Refl <- eq
  = case t of
      TInt -> ()
      -- TBool -> ()

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              ( Bug3.hs, interpreted )

Bug3.hs:15:5: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: TBool
   |
15 |   = case t of
   |     ^^^^^^^^^...

Stunning.

It turns out that when GHC desugars patterns bound by pattern guards, it completely forgets to update the local dictionaries in scope with addDictsDs! I have no idea how this oversight went unnoticed for so long... In any case, I have a patch for this at D4968.

Trac metadata

Trac field	Value
Differential revisions	- → D4968

Gah. The deeper I dig the less happy I am. The addDictsDs is ok, but I'm worried about genCaseTmCs1 and genCaseTmCs2

The basic idea here is that when we see (in source Haskell)

   case x of { (a, Just b) -> blah }

we want to desugar blah in the knowledge that

   x ~ (a, Just b)

Reason: suppose that somewhere inside blah we see

     case x of { (a, Nothing) -> blah2 }

Then we want to declare this branch as unreachable.

But what if the original expression was

   case x of (a, Just _) -> blah

Now what equality do we generate? Maybe we make a fresh variable? And maybe that is waht we want. This conversion from a pattern to a PmExpr is all hidden inside the cryptic line

  [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p

I have very little idea of what this does.

Returning to our case expression, we'll end up using genCaseTmCs2 in matchWrapper. And that seems to generate two equalities

  v ~ (a, Just b)
  v ~ x

That seems terribly indirect, although perhaps not actually wrong. I suppose that it might work in cases like

   case (p,q) of (a, Just b) -> blah

but they probably never happen -- and at very least it could do with explanation.

Bottom line so far: no actual bugs, but pretty tough going.

To be clear, the problems you're describing in ticket:15385#comment:157379 aren't unique to pattern guards, but rather anything that generates term equalities for the coverage checker (which includes case expressions)?

To be clear, the problems you're describing in ticket:15385#comment:157379 aren't unique to pattern guards, but rather anything that generates term equalities for the coverage checker (which includes case expressions)?

Correct, yes.

OK. Well, I simply went along with the status quo (adapting from the code for case expressions in matchWrapper) when writing D4968. At the very least, I'd like to get that patch in to 8.6, and then perhaps we can revisit the design of term equalities later.

Yes fine. I've commented on Phab.

And I've replied on Phab. (Unfortunately, Phab notifications appear to be dysfunctional at the moment...)

mentioned in commit 45cfe651

mentioned in commit 9d388eb8

This fixes a pretty serious incompleteness in the pattern-match coverage checker, so I'd humbly request that the commits in #15385 (closed) and #15385 (closed) be merged to 8.6.

Trac metadata

Trac field	Value
Test case	- → pmcheck/should_compile/T15385

added 1 deleted label

closed

#15385 (closed) merged in 42c51e2f, #15385 (closed) in e649085b.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added pattern match warnings label

added Pnormal label