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

[GHC]

#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 cactus):

 I have no idea what the proposal is anymore... which I find a bit
 worrying, given I am supposed to implement it.

 Right now, on `master` as of `6f818e08`, this is the behaviour you get:


 {{{
 {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
 module ShouldCompile where

 data X b where
   Y :: [a] -> X (Maybe a)

 pattern C1 :: [a] -> X (Maybe a)
 pattern C1 x <- Y x

 pattern C2 x <- Y x

 pattern C3 :: (t ~ Maybe a) => [a] -> X t
 pattern C3 x <- Y x

 }}}

 with this setup, you get


 {{{
 λ» :i C1
 pattern C1 :: [a] -> X (Maybe a)        -- Defined at T9953-3.hs:8:9
 λ» :i C2
 pattern C2 :: t ~ Maybe a => [a] -> X t
         -- Defined at T9953-3.hs:10:9
 λ» :i C3
 pattern C3 :: t ~ Maybe a => [a] -> X t
         -- Defined at T9953-3.hs:13:9
 }}}

 Isn't this exactly the behaviour specified by Simon's latest comment?

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