COMPLETE sets don't interact well with type family-returning pattern synonyms
Originally reported by greatBigDot628 here.
COMPLETE
sets don't quite appear to work when a pattern synonym in the set returns a type family. Consider the following example of this:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
import Data.Kind
import Unsafe.Coerce
type family Sing :: k -> Type
class SingI a where
sing :: Sing a
data SingInstance :: forall k. k -> Type where
SingInstance :: SingI a => SingInstance a
newtype DI (a :: k) = Don'tInstantiate (SingI a => SingInstance a)
singInstance :: forall k (a :: k). Sing a -> SingInstance a
singInstance s = with_sing_i SingInstance
where
with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
with_sing_i si = unsafeCoerce (Don'tInstantiate si) s
{-# COMPLETE Sing #-}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern Sing <- (singInstance -> SingInstance)
where Sing = sing
-----
data SBool :: Bool -> Type where
SFalse :: SBool False
STrue :: SBool True
type instance Sing = SBool
f :: SBool b -> ()
f Sing = ()
g :: Sing (b :: Bool) -> ()
g Sing = ()
If you compile this with GHC 8.10.1 or HEAD, it will report f
and g
as non-exhaustive, despite the fact that they match on the Sing
COMPLETE
set:
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:43:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘f’:
Patterns not matched:
SFalse
STrue
|
43 | f Sing = ()
| ^^^^^^^^^^^
Bug.hs:46:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘g’:
Patterns not matched:
SFalse
STrue
|
46 | g Sing = ()
| ^^^^^^^^^^^
This appears to be a regression from GHC 8.8.3, which does not report any warnings at all.
The fact that the Sing
pattern synonym returns a type family appears to be crucial. If you define a variant of Sing
that returns a concrete data type, for instance:
{-# COMPLETE SingBool #-}
pattern SingBool :: forall (b :: Bool). () => SingI b => SBool b
pattern SingBool = Sing
fSingBool :: SBool b -> ()
fSingBool SingBool = ()
gSingBool :: Sing (b :: Bool) -> ()
gSingBool SingBool = ()
Then the warnings go away. cc @sgraf812