
Yes, ok, but should this information be necessary to provide with the
#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): Replying to [comment:8 kosmikus]: pattern synonym? Isn't this something that should be derived from the type signature of the function in which it is used? Yes, it should be provided with the pattern synonym. No, it should not be derived form the use. Here's why. As you go on to show, the "derive from use" idea is more flexible, '''but it is fundamentally non-modular''': you can only understand when a pattern synonym will typecheck by expanding it! The whole point about pattern synonyms is that you ''don't'' need to think about their implementation (expansion); you can reason about them using only their interface. To take an analogy, go back to GADTs: {{{ data T a where T1 :: T Bool T2 :: T Char f T1 = True }}} Does `f :: T a -> Bool` or `f :: T a -> a`? You could say "look to the uses". Here are two calls {{{ (f 'x' && True) -- Needs f :: T a -> Bool (ord (f 'x')) -- Needs f :: T a -> a }}} If you inline `f` (akin to expanding the pattern synonym), you can make both typecheck. But we don't inline functions: we give them a single, principal type, and use that at every call site. It's just the same with pattern synonyms. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler