Inconsistent pattern-match warnings when using guards versus case expressions

changed milestone to %8.8.1

changed weight to 5

Here is a slightly smaller example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Data.Void (Void)

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True
data SUnit :: () -> Type where
  SUnit :: SUnit '()

type family IsUnit (u :: ()) :: Bool where
  IsUnit '() = True

sIsUnit :: SUnit u -> SBool (IsUnit u)
sIsUnit SUnit = STrue

type family If (c :: Bool) (t :: Type) (f :: Type) :: Type where
  If True  t _ = t
  If False _ f = f

type family F (u1 :: ()) (u2 :: ()) :: Type where
  F u1 u2 =
    If (IsUnit u1) (Case u2) Int

type family Case (u :: ()) :: Type where
  Case '() = Int

g1 :: F u1 u2 :~: Char
   -> SUnit u1 -> SUnit u2
   -> Void
g1 Refl su1 su2
  | STrue <- sIsUnit su1
  = case su2 of {}

g2 :: F u1 u2 :~: Char
   -> SUnit u1 -> SUnit u2
   -> Void
g2 Refl su1 su2
  = case sIsUnit su1 of
      STrue ->
        case su2 of {}

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

Bug.hs:40:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘g1’: Patterns not matched: Refl _ _
   |
40 | g1 Refl su1 su2
   | ^^^^^^^^^^^^^^^...
Ok, one module loaded.

At the time of this writing, after !963 (closed) this will generate the following warnings:

test.hs:40:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘g1’: g1 Refl su1 su2 = ...
   |
40 | g1 Refl su1 su2
   | ^^^^^^^^^^^^^^^...

test.hs:47:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘g2’: g2 Refl su1 su2 = ...
   |
47 | g2 Refl su1 su2
   | ^^^^^^^^^^^^^^^...

Edit: This should probably warn about inaccessible RHS instead... Edit2: Well, no. A call site like g2 undefined undefined undefined should result in a type error. Edit3: Gah, ignore my ramblings. The above error messages are wrong, of course such a call site is possible. Will investigate what's wrong here.

Which look correct to me, since F () () will evaluate to Int, not to Char. If I replace the mentions of Char with Int, I get the following warnings:

test.hs:42:5: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: SUnit
   |
42 |   = case su2 of {}
   |     ^^^^^^^^^^^^^^

test.hs:48:5: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: SFalse
   |
48 |   = case sIsUnit su1 of
   |     ^^^^^^^^^^^^^^^^^^^...
                                                                                                                                                                                                                                             test.hs:50:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive                                                                                                                                                                                                         In a case alternative: Patterns not matched: SUnit
   |
50 |         case su2 of {}
   |         ^^^^^^^^^^^^^^

The first one probably makes for the better regression test T15753c?

Even simpler:

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

import Data.Type.Equality

data G a where
  GInt  :: G Int
  GBool :: G Bool

ex1, ex2, ex3
  :: a :~: Int
  -> G a
  -> ()

ex1 Refl g
  | GInt <- id g
  = ()

ex2 Refl g
  | GInt <- g
  = ()

ex3 Refl g
  = case id g of
      GInt -> ()

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

Bug.hs:17:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘ex1’: Patterns not matched: Refl _
   |
17 | ex1 Refl g
   | ^^^^^^^^^^...

This time, I've included three examples. In particular, note that ex1 and ex2 are //extremely// similar—the only difference is the use of id!

Since !963 (closed), for the better or the worse, will not discard any guards with a 'complex' (PmExprOther) RHS anymore, this testcase T15753a will be fixed.

A workaround is to bind the result of id g to some auxiliary variable. For instance, both of the following variants of ex1 are deemed to be exhaustive:

ex1a, ex1b
  :: a :~: Int
  -> G a
  -> ()

ex1a Refl g
  | let g' = id g
  , GInt <- g'
  = ()

ex1b Refl g
  | g' <- id g
  , GInt <- g'
  = ()

mentioned in issue #15884 (closed)

Trac metadata

Trac field	Value
Related	- → #15884 (closed)

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

mentioned in issue #16129 (closed)

#16129 (closed) is ~~possibly~~ (EDIT: //definitely//) related:

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Bug where

import Data.Functor.Identity

{-# COMPLETE Id #-}
pattern Id :: a -> Identity a
pattern Id x = Identity x

class Hm a where
  hm :: a -> a
instance Hm (Identity a) where
  hm = id

bug, workaround1, workaround2 :: Identity a -> a
bug ia
  | Id a <- hm ia
  = a

workaround1 ia
  | let ia' = hm ia
  , Identity a <- ia'
  = a

workaround2 ia = a
  where Id a = hm ia

$ ghci Bug.hs -Wincomplete-patterns
GHCi, version 8.6.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:17:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘bug’: Patterns not matched: _
   |
17 | bug ia
   | ^^^^^^...

Trac metadata

Trac field	Value
Related	#15884 (closed) → #15884 (closed), #16129 (closed)

Replying to [ticket:15753#comment:166786 RyanGlScott]:

Not sure if this is a useful reduction:

{-# LANGUAGE PatternSynonyms #-}
module Bug where

{-# COMPLETE Id #-}
pattern Id :: () -> ()
pattern Id a = a

bug :: () -> ()
bug ia
  | Id a <- id ia
  = a

Another (tiny) reduction:

{-# LANGUAGE PatternSynonyms #-}
module Bug where

{-# COMPLETE Id #-}
pattern Id :: ()
pattern Id = ()

bug :: ()
bug | Id <- id () = ()

Bug.hs:9:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘bug’: Guards do not cover entire pattern space
  |
9 | bug | Id <- id () = ()
  | ^^^^^^^^^^^^^^^^^^^^^^

Given that it takes so little to run into this bug (see ticket:15753#comment:166800), should its priority maybe be high instead?

Trac metadata

Trac field	Value
CC	- → sjakobi

added pattern match warnings label

added error messages label

marked this issue as related to #11245 (closed)

assigned to @sgraf812

The problem here is that bug is analysed both with checkSingle (which doesn't complain) and with checkMatches, which complains about a single uncovered value vector abstraction [] (is this even a thing?) using the Builtin complete set from the data declaration.

The problem (EDIT: for the last reproduction) is that singleConstructor doesn't account for pattern synonym and singleton COMPLETE sets.

mentioned in commit 0bba7c0c

mentioned in merge request !699 (merged)

mentioned in commit b1613985

mentioned in commit 9108ead1

So, to sum up what leads to the confusing warning:

Prior to the algorithm from the paper, we have to abstract type-checked HsExprs into PmExprs.
When we encounter a pattern guard such as GInt <- id (), this abstraction step is handled by mkGuard (and translateGuards, I think).
We first check if GInt is an obvious singleMatchConstructor, which it isn't. (Yet, the algorithm from the paper would integrate the constraint from Refl and be able to see that GInt is the only possible match.)
Next, we check if the guard expression has a useful counter-part as a PmExpr. Notably, a function application does not and gets abstracted into a PmOtherExpr, for the simple reason that "the term oracle doesn't cope with applications". This also happens for view patterns and other guards (see Note [Guards and Approximation]).
An useless guard expression (PmOtherExpr) gets abstracted by a conservative fake_pat of the form True <- _, which is always incomplete, leading to the warning

Ironically, the same doesn't happen if we bind the function application in a let before: | let g' = id g is abstracted by a complete pattern guard | g' <- id g, so no approximation happening there. Crucially, the original GInt <- id g becomes GInt <- g' and the guard expression can be abstracted by PmVar. No conservative approximation necessary here, either.

I discussed the issue with @simonpj. He said it's a shame that we give up before we even pass the expression on to the algorithm.

The simplest way to solve this particular ticket is probably to always bind complex guard expressions to fresh names. But that won't get us very far, because still can't handle stuff like

foo
  | Just _ <- id Nothing
  = 42
  | Nothing <- id Nothing
  = 43

Where both id Nothing expressions would be bound to different names.

A possible way out is to perform an on-the-fly "global value numbering", by desugaring complex pattern guards to Core expressions and look up their value number (which we could just represent as a fresh binder, virtually binding the common sub-expression) in a CoreMap. The term oracle still doesn't need to handle function application, but we properly common up expressions in a way that it can just match on variables. Even better: the term oracle can decide to look into the definition of a variable if there ever is the need in the future.

Also I should add that #15753 (comment 166800) is fixed by !699 (merged).

mentioned in commit f4702404

mentioned in commit 6665a30d

mentioned in commit d236d9d0

He said it's a shame that we give up before we even pass the expression on to the algorithm

Yes, it's a terrible shame! Let's just desugar to Core, possibly run the very simple optimiser in CoreOpt, and then have an oracle that makes best efforts to determine equality or inequality of Core expressions.

I think your comment about global value numbering is essentially this approach, correct?

At worst we do no worse than now, but we have the opportunity to do better by making the oracle better

I realised it's a little tricky to handle overloaded literals this way.

If I understand the plan right, we would no longer see overloaded literals at the Core level, where they should already have been desugared to calls to fromInteger.

Thinking about it, this might not actually be a bad thing, because this naturally resolves the Note [Undecidable Equality for Overloaded Literals] issue by appealing to congruence. I.e., we know fromInteger 1 == fromInteger 1, but we don't know anything about whether fromInteger 1 == fromInteger 2 is true. It might have detrimental effect on efficiency, but let's not yet worry about that.

I think your comment about global value numbering is essentially this approach, correct?

Yes, global value numbering is just a possible strategy to implement the equality decision procedure.

added Pnormal label

Incidentally this didn't need any of the discussed smartness around identifying semantically equivalent RHS (as opposed to #15884 (closed)) of guards, just not dropping any guards as in !963 (closed) is enough. The OP doesn't produce any warnings any more.

mentioned in commit 567995d8

mentioned in commit f6e8ef3c

mentioned in commit 72d0cbf3

mentioned in commit 1725713c

mentioned in commit 1c821883

mentioned in commit 4443bbf0

mentioned in commit 6e812c87

mentioned in commit 60048c5c

mentioned in commit 7d6ce6d6

mentioned in commit e40ab2c8

mentioned in commit 89e7b6af

mentioned in commit e6c47536

mentioned in commit c6bdda70

mentioned in commit e67a1a0b

mentioned in commit a2c03c09

mentioned in commit a55d570a

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

Inconsistent pattern-match warnings when using guards versus case expressions

Child items ...

Activity

Inconsistent pattern-match warnings when using guards versus case expressions

Relates to

Activity