[GHC] #14059: COMPLETE sets don't work at all with data family instances
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms, | PatternMatchWarnings | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's some code that uses a pattern synonym for a data family GADT constructor, along with a corresponding `COMPLETE` set: {{{#!hs {-# 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`: {{{#!hs {-# 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 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: mpickering (added) Comment: 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., {{{#!hs {-# 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: {{{#!hs {-# 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: {{{#!hs {-# COMPLETE SFalse, STrue :: Sing (z :: Bool) #-} }}} {{{ Bug.hs:20:47: error: parse error on input ‘(’ | 20 | {-# COMPLETE SFalse, STooGoodToBeTrue :: Sing (z :: Bool) #-} | }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs 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: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Keep walking down the path in comment:2. That looks like a promising direction. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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) #-}`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Unfortunately, this means that the non-data-family instance version has also //regressed//. That is to say, this program: {{{#!hs {-# 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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 [http://git.haskell.org/ghc.git/blob/857005a762a12e021c3cc65b729bd6263b7145fb... this criterion]: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: => Phab:D4752 Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14059: COMPLETE sets don't work at all with data family instances
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.1
Resolution: | Keywords:
| PatternSynonyms,
| PatternMatchWarnings
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: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
participants (1)
-
GHC