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
comment:2 Changed 11 months ago by
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
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
Related Tickets: | → #15884 |
---|
comment:5 Changed 9 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
comment:6 follow-up: 7 Changed 9 months ago by
Related Tickets: | #15884 → #15884, #16129 |
---|
#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 | ^^^^^^...
comment:7 Changed 9 months ago by
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
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
Cc: | sjakobi added |
---|
Given that it takes so little to run into this bug (see comment:8), should its priority maybe be high
instead?
Here is a slightly smaller example: