[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 goldfire):

 Replying to [comment:9 simonpj]:
 > In short, if you want GADT-like behaviour for a pattern synonym, you can
 get it ''only'' by giving explicit equality constraints in the signature,
 and not by having a complex result type (as you can do for real data
 constructors).

 Yech. This means that declaring a pattern synonym for a GADT data
 constructor requires writing the type differently than the idiomatic way
 to do it for data constructors.

 I think a second '''principle''' might be this: The type signature for a
 pattern should mean the same thing that it would for a data constructor.

 It strikes me that this problem is precisely the same as the required vs.
 produced distinction. In your `P2`, `t ~ Maybe a` is a requirement; in
 your `P1`, it's provided.

 I don't have a better concrete suggestion at the moment, sadly.

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