#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