Opened 11 months ago

Last modified 7 days ago

#15753 new bug

Inconsistent pattern-match warnings when using guards versus case expressions

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.6.1
Keywords: PatternMatchWarnings Cc: sjakobi
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #15884, #16129 Differential Rev(s):
Wiki Page:

Description

Consider the following code (apologies for the rather non-minimal example):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
module Bug where

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

data family Sing :: forall k. k -> Type
data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True
data instance Sing :: forall a. [a] -> Type where
  SNil  :: Sing '[]
  SCons :: Sing x -> Sing xs -> Sing (x:xs)
data instance Sing :: forall a b. (a, b) -> Type where
  STuple2 :: Sing x -> Sing y -> Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
  SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (f :: k1 ~> k2) @@ (x :: k1) :: k2
infixl 9 @@

newtype Map k v = MkMap [(k, v)]
data instance Sing :: forall k v. Map k v -> Type where
  SMkMap :: Sing x -> Sing (MkMap x)

type family MapEmpty :: Map k v where
  MapEmpty = MkMap '[]

type family MapInsertWith (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v) :: Map k v where
  MapInsertWith _ new_k new_v (MkMap '[]) = MkMap '[ '(new_k, new_v)]
  MapInsertWith f new_k new_v (MkMap ('(old_k,old_v):old_kvs)) =
    If (old_k == new_k)
       (MkMap ('(new_k,f @@ new_v @@ old_v):old_kvs))
       (Case (MapInsertWith f new_k new_v (MkMap old_kvs)) old_k old_v)

type family Case (m :: Map k v) (old_k :: k) (old_v :: v) :: Map k v where
  Case (MkMap kvs) old_k old_v = MkMap ('(old_k,old_v) : kvs)

sMapInsertWith :: forall k v (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v).
                  SEq k
               => Sing f -> Sing new_k -> Sing new_v -> Sing m
               -> Sing (MapInsertWith f new_k new_v m)
sMapInsertWith _  snew_k snew_v (SMkMap SNil) = SMkMap (STuple2 snew_k snew_v `SCons` SNil)
sMapInsertWith sf snew_k snew_v (SMkMap (STuple2 sold_k sold_v `SCons` sold_kvs)) =
  case sold_k %== snew_k of
    STrue -> SMkMap (STuple2 snew_k (sf @@ snew_v @@ sold_v) `SCons` sold_kvs)
    SFalse ->
      case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of
        SMkMap skvs -> SMkMap (STuple2 sold_k sold_v `SCons` skvs)

class PEq a where
  type (x :: a) == (y :: a) :: Bool
class SEq a where
  (%==) :: forall (x :: a) (y :: a).
           Sing x -> Sing y -> Sing (x == y)

mapInsertWithNonEmpty1 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
                                     (new_k :: k) (new_v :: v) (m :: Map k v).
                          SEq k
                       => Sing f -> Sing new_k -> Sing new_v -> Sing m
                       -> m :~: MkMap ('(old_k,old_v) : old_kvs)
                       -> MapInsertWith f new_k new_v m :~: MapEmpty
                       -> Void
mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
  | STuple2 sold_k _ `SCons` sold_kvs <- sm
  , SFalse <- sold_k %== snew_k
  = case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}

mapInsertWithNonEmpty2 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
                                     (new_k :: k) (new_v :: v) (m :: Map k v).
                          SEq k
                       => Sing f -> Sing new_k -> Sing new_v -> Sing m
                       -> m :~: MkMap ('(old_k,old_v) : old_kvs)
                       -> MapInsertWith f new_k new_v m :~: MapEmpty
                       -> Void
mapInsertWithNonEmpty2 sf snew_k snew_v (SMkMap sm) Refl Refl
  | STuple2 sold_k _ `SCons` sold_kvs <- sm
  = case sold_k %== snew_k of
      SFalse ->
        case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}

If you compile this with GHC 8.6.1 or later, you'll notice something interesting happening with the pattern-match coverage checker warnings:

$ /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:78:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘mapInsertWithNonEmpty1’:
        Patterns not matched: _ _ _ (SMkMap _) Refl Refl
   |
78 | mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Ok, one module loaded.

mapInsertWithNonEmpty1 is deemed non-exhaustive, but mapInsertWithNonEmpty2 is deemed exhaustive. However, the code for the two functions are functionally identical—the only difference is that mapInsertWithNonEmpty1 uses one more pattern guard than mapInsertWithNonEmpty2 does.

Change History (11)

comment:1 Changed 11 months ago by RyanGlScott

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.

comment:2 Changed 11 months ago by RyanGlScott

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!

comment:3 Changed 11 months ago by RyanGlScott

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'
  = ()

comment:4 Changed 11 months ago by RyanGlScott

comment:5 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:6 Changed 9 months ago by RyanGlScott

#16129 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
   | ^^^^^^...
Last edited 9 months ago by RyanGlScott (previous) (diff)

comment:7 in reply to:  6 Changed 9 months ago by sjakobi

Replying to 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

comment:8 Changed 9 months ago by sjakobi

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 () = ()
  | ^^^^^^^^^^^^^^^^^^^^^^

comment:9 Changed 8 months ago by sjakobi

Cc: sjakobi added

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

comment:10 Changed 6 months ago by Marge Bot <ben+marge-bot@…>

In d236d9d0/ghc:

Make `singleConstructor` cope with pattern synonyms

Previously, `singleConstructor` didn't handle singleton `COMPLETE` sets
of a single pattern synonym, resulting in incomplete pattern warnings
in #15753.

This is fixed by making `singleConstructor` (now named
`singleMatchConstructor`) query `allCompleteMatches`, necessarily making
it effectful. As a result, most of this patch is concerned with
threading the side-effect through to `singleMatchConstructor`.

Unfortunately, this is not enough to completely fix the original
reproduction from #15753 and #15884, which are related to function
applications in pattern guards being translated too conservatively.

comment:11 Changed 7 days ago by Marge Bot <ben+marge-bot@…>

In 7915afc/ghc:

Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

-------------------------
Metric Decrease:
    ManyAlternatives
    T11195
-------------------------
Note: See TracTickets for help on using tickets.