Opened 3 weeks ago

Last modified 2 weeks ago

#14059 new bug

COMPLETE sets don't work at all with data family instances

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: PatternSynonyms, PatternMatchWarnings Cc: mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Change History (3)

comment:1 Changed 2 weeks ago by RyanGlScott

Cc: mpickering added

Here's one architectural issue: COMPLETE sets currently aren't designed with data family instances in mind. Why? Because you can optionally give the name of a tycon for a COMPLETE set, e.g.,

{-# COMPLETE False, TooGoodToBeTrue :: Boolean #-}

However, this necessarily needs to be more involved for data family instances, because we're dealing with a proper type, not just a tycon. Put differently, it wouldn't be enough to say:

{-# COMPLETE SFalse, STrue :: Sing #-}

This is wrong, since we don't want a COMPLETE set for Sing (a :: k), we want a COMPLETE set for Sing (a :: Bool). But GHC won't let us use:

{-# COMPLETE SFalse, STrue :: Sing (z :: Bool) #-}
Bug.hs:20:47: error: parse error on input ‘(’
   |
20 | {-# COMPLETE SFalse, STooGoodToBeTrue :: Sing (z :: Bool) #-}
   |

comment:2 Changed 2 weeks ago by RyanGlScott

I looked into this some more tonight. While I wasn't able to find the underlying cause of why COMPLETE sets don't seem to quite work for data family instances, I did notice a discrepancy between pattern synonyms for datatype contructors and those for data family instance constructors. In several places throughout GHC, the conLikeResTy function is used to determine the return type of a conlike (be it a proper data constructor or a pattern synonym).

For datatype constructors, conLikeResTy returns something of the form T a1 ... an, where T is a datatype tycon. This holds true regardless of whether conLikeResTy is called on a proper data constructor (e.g., the MkT in data T a = MkT a) or a pattern synonym for a data constructor (e.g., pattern FakeT a = MkT a).

With data family instances, however, the story is a little different. Let's suppose we have:

data family F a b
data instance F Int b = MkF Int
pattern FakeF a = MkF a

If you call conLikeResTy on MkF, you won't get F Int b, but instead something like R:FInt b, where R:FInt is the representation tycon for the data family instance F Int b (as opposed to F, which is the parent data family tycon). However, calling conLikeResTy on FakeF gives you F Int b instead!

That's a difference that smells quite funny to me, but I haven't tracked down the scent's origin yet. For what it's worth, COMPLETE sets group conlikes by parent tycon name, not by representation tycon name, so for instance:

{-# COMPLETE SFalse, STooGoodToBeTrue :: Sing #-}

In order to look up these conlikes, you'd need to use Sing (z :: Bool), not R:SingzBool (type weirdness in comment:1 aside). What does it all mean? I can't be sure at the moment.

comment:3 Changed 2 weeks ago by goldfire

Keep walking down the path in comment:2. That looks like a promising direction.

Note: See TracTickets for help on using tickets.