[GHC] #14059: COMPLETE sets don't work at all with data family instances

30 Jul 2017


      #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