Opened 11 months 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): Phab:D4752
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 (9)

comment:1 Changed 11 months 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 11 months 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 11 months ago by goldfire

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

comment:4 Changed 9 months ago by RyanGlScott

https://ghc.haskell.org/trac/ghc/ticket/14135#comment:9 offers some peace of mind for one problem I encountered in comment:2 (where I bemoaned the fact that I can only write {-# COMPLETE SFalse, STooGoodToBeTrue :: Sing #-} (and not {-# COMPLETE SFalse, STooGoodToBeTrue :: Sing (z :: Bool) #-}).

comment:5 Changed 3 weeks ago by RyanGlScott

Evidently, this changed a bit from GHC 8.2 to 8.4. In 8.4, you actually do get a warning about wobble:

$ /opt/ghc/8.4.2/bin/ghci Bug.hs
GHCi, version 8.4.2: 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
   | ^^^^^^^^^^^^^^^^^^^

Bug.hs:26:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘wobble’: Patterns not matched: _
   |
26 | wobble STooGoodToBeTrue = True
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Still, this doesn't seem quite right, as the warning says Patterns not matched: _ instead of Patterns not matched: SFalse, like its counterpart wibble.

comment:6 Changed 3 weeks ago by RyanGlScott

Unfortunately, this means that the non-data-family instance version has also regressed. That is to say, this program:

{-# 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

Used to give the right warning in GHC 8.2 (as shown in the original description), but on GHC 8.4, it now demonstrates the same problem as in the version with data families:

$ /opt/ghc/8.4.2/bin/ghci Foo.hs
GHCi, version 8.4.2: 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: _
   |
23 | wobble STooGoodToBeTrue = True
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I suppose the uniformity is comforting, at least...

comment:7 Changed 3 weeks ago by RyanGlScott

OK, I at least know why the error messages are different in GHC 8.4. It's due to the fix for #14135, which filters out candidate conlikes from COMPLETE sets with this criterion:

      isValidCompleteMatch :: Type -> [ConLike] -> Bool
      isValidCompleteMatch ty =
        isJust . mapM (flip tcMatchTy ty . resTy . conLikeFullSig)
        where
          resTy (_, _, _, _, _, _, res_ty) = res_ty

I believe this criterion is too conservative, since it requires the type of every conlike in a COMPLETE set to match the type of the scrutinee. But that assumption doesn't hold true when one of the conlikes is for a GADT constructor, as in the second example from the description:

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 #-}

wobble :: SBool z -> Bool
wobble STooGoodToBeTrue = True

Here, the type of the scrutinee in wobble is SBool z, but the type of the first conlike in the COMPLETE set is SBool False, so tcMatchTy (SBool False) (SBool z) will return Nothing, which means we filter out that COMPLETE set entirely. This is terrible, since SFalse can be pattern-matched on in wobble!

This leads me to believe that we should only be performing this tcMatchTy check on pattern synonym constructors, not data constructors. I applied this change to isValidCompleteMatch locally and sure enough, the error message in this ticket went back to what is was in 8.2. I'll prepare a patch with this payload before investigating the underlying issue in this ticket further.

comment:8 Changed 3 weeks ago by RyanGlScott

Differential Rev(s): Phab:D4752

Phab:D4752 fixes the issue discovered starting at comment:5. As mentioned earlier, it does not fix the entirety of #14059, but this patch at least restores the error message back to what it was in 8.2.

comment:9 Changed 2 weeks ago by Ben Gamari <ben@…>

In 4d80044/ghc:

Fix a bad interaction between GADTs and COMPLETE sets

As observed in #14059 (starting at comment 5), the error
messages surrounding a program involving GADTs and a `COMPLETE` set
became worse between 8.2 and 8.4. The culprit was a new validity
check in 8.4 which filters out `COMPLETE` set candidates if a return
type of any conlike in the set doesn't match the type of the
scrutinee. However, this check was too conservative, since it removed
perfectly valid `COMPLETE` sets that contained GADT constructors,
which quite often have return types that don't match the type of a
scrutinee.

To fix this, I adopted the most straightforward possible solution of
only performing this validity check on //pattern synonym//
constructors, not //data// constructors.

Note that this does not fix #14059 entirely, but instead simply fixes
a particular buglet that was discovered in that ticket.

Test Plan: make test TEST=T14059

Reviewers: bgamari, mpickering

Reviewed By: mpickering

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14059

Differential Revision: https://phabricator.haskell.org/D4752
Note: See TracTickets for help on using tickets.