Re: [GHC] #9953: Pattern synonyms don't work with GADTs

8 Jan 2015

      #9953: Pattern synonyms don't work with GADTs
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                   Owner:  cactus
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:  7.10.1
       Component:  Compiler (Type    |                 Version:  7.10.1-rc1
  checker)                           |                Keywords:
      Resolution:                    |  PatternSynonyms
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Here's the example in play:

 {{{
 data T1 a where
    MkT1 :: a -> T1 (Maybe a)

 -- Inferred type pattern P1 :: (t ~ Maybe a) => a -> T t
 pattern P1 x <- MkT x

 -- Inferred type pattern P2 :: a -> [Maybe a]
 pattern P2 x <- [Just x]
 }}}

 Couldn't we write these type signatures as

 {{{
 pattern P1 :: (t ~ Maybe a) => () => a -> T  t
 pattern P2 :: () => (t ~ Maybe a) => a -> [t]
 }}}

 ?

 And, I disagree with Simon's conclusion that we cannot have pattern type
 signatures mean the same as data constructor signatures. We could decide
 than any non-uniformity in the result type of a pattern signature means a
 provided equality, just like a GADT. Then, the syntax of the type for `P2`
 would have to change to something else -- after all, `P2` is not the
 synonym of any valid data constructor.

 As we're thinking about this, it strikes me that there is some
 relationship between the current debate and the distinction between GADTs
 and data families. For example:

 {{{
 data G a where
   MkGInt :: G Int

 data family H a
 data instance H Int where
   MkHInt :: H Int
 }}}

 `MkGInt` is a GADT constructor that provides an equality when matching.
 `MkHInt`, on the other hand, '''requires''' the equality when matching.
 Yet both have the same type signature. So, something a little confusing is
 going on here. Do pattern synonyms work properly with data families?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler