#15385 closed bug (fixed)

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: pmcheck/should_compile/T15385
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4968
Wiki Page:

Description

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.

Change History (12)

comment:1 Changed 14 months ago by RyanGlScott

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.

comment:2 Changed 14 months ago by RyanGlScott

Differential Rev(s): Phab:D4968
Status: newpatch

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 Phab:D4968.

comment:3 Changed 14 months ago by simonpj

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.

comment:4 Changed 14 months ago by RyanGlScott

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

comment:5 Changed 14 months ago by simonpj

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

Correct, yes.

comment:6 Changed 14 months ago by RyanGlScott

OK. Well, I simply went along with the status quo (adapting from the code for case expressions in matchWrapper) when writing Phab: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.

comment:7 Changed 14 months ago by simonpj

Yes fine. I've commented on Phab.

comment:8 Changed 14 months ago by RyanGlScott

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

comment:9 Changed 14 months ago by Simon Peyton Jones <simonpj@…>

In 45cfe651/ghc:

Small refactor in desugar of pattern matching

In reviewing Phab:D4968 for Trac #15385 I saw a small
but simple refactor to avoid unnecessary work in the
desugarer.

This patch just arranges to call
   matchSinglePatVar v ...
rather than
   matchSinglePat (Var v) ...

The more specialised function already existed, as
   match_single_pat_var

I also added more comments about decideBangHood

comment:10 Changed 14 months ago by Ryan Scott <ryan.gl.scott@…>

In 9d388eb8/ghc:

Fix #15385 by using addDictsDs in matchGuards

Summary:
When coverage checking pattern-matches, we rely on the call
sites in the desugarer to populate the local dictionaries and term
evidence in scope using `addDictsDs` and `addTmCsDs`. But it turns
out that only the call site for desugaring `case` expressions was
actually doing this properly. In another part of the desugarer,
`matchGuards` (which handles pattern guards), it did not update the
local dictionaries in scope at all, leading to #15385.

Fixing this is relatively straightforward: just augment the
`BindStmt` case of `matchGuards` to use `addDictsDs` and `addTmCsDs`.
Accomplishing this took a little bit of import/export tweaking:

* We now need to export `collectEvVarsPat` from `HsPat.hs`.
* To avoid an import cycle with `Check.hs`, I moved `isTrueLHsExpr`
  from `DsGRHSs.hs` to `DsUtils.hs`, which resides lower on the
  import chain.

Test Plan: make test TEST=T15385

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15385

Differential Revision: https://phabricator.haskell.org/D4968

comment:11 Changed 14 months ago by RyanGlScott

Status: patchmerge
Test Case: pmcheck/should_compile/T15385

This fixes a pretty serious incompleteness in the pattern-match coverage checker, so I'd humbly request that the commits in comment:9 and comment:10 be merged to 8.6.

comment:12 Changed 14 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.