COMPLETE sets don't work at all with data family instances
Here's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding COMPLETE
set:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
data family Sing (a :: k)
data instance Sing (z :: Bool) where
SFalse :: Sing False
STrue :: Sing True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> Sing z
pattern STooGoodToBeTrue = STrue
{-# COMPLETE SFalse, STooGoodToBeTrue #-}
wibble :: Sing (z :: Bool) -> Bool
wibble STrue = True
wobble :: Sing (z :: Bool) -> Bool
wobble STooGoodToBeTrue = True
However, if you compile this, you might be surprised to find out that GHC only warns about wibble
being non-exhaustive:
$ ghci Bug.hs
GHCi, version 8.2.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:23:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse
|
23 | wibble STrue = True
| ^^^^^^^^^^^^^^^^^^^
I believe the use of data families is the culprit here, since a variant of this program which doesn't use data families correctly warns for both wibble
and wobble
:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Foo where
data SBool (z :: Bool) where
SFalse :: SBool False
STrue :: SBool True
pattern STooGoodToBeTrue :: forall (z :: Bool). ()
=> z ~ True
=> SBool z
pattern STooGoodToBeTrue = STrue
{-# COMPLETE SFalse, STooGoodToBeTrue #-}
wibble :: SBool z -> Bool
wibble STrue = True
wobble :: SBool z -> Bool
wobble STooGoodToBeTrue = True
$ ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:20:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘wibble’: Patterns not matched: SFalse
|
20 | wibble STrue = True
| ^^^^^^^^^^^^^^^^^^^
Foo.hs:23:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘wobble’: Patterns not matched: SFalse
|
23 | wobble STooGoodToBeTrue = True
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |