
#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by simonpj): Yes, I think it would have to be the latter. Several open issues remain: * We need pattern signatures. The workaround (of a signature embedded in the pattern) doesn't work too well for these more complicated types. * In fact having signatures embedded in a pattern synonym is problematic, because signatures behave differently in patterns and in terms. {{{ g x = Just x :: Maybe a f (Just x :: Maybe a) = x }}} In `g`, the type signature is implicitly quantified, so it really means `Just x :: forall a. Maybe a`, and the definition will therefore be rejected. But in the definition of `f`, the 'a' in the pattern is a ''binding'' occurrence, that scopes over the RHS; there is no implicit quantification. I'm inclined simply to disallow signature in the RHS of a pattern synonym. * We have no good syntax for the required/provided issue. I thought this was written up on the [wiki:PatternSynonyms Pattern Synonym wiki page] but it isn't. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler