[GHC] #8968: Pattern synonyms and GADTs

[GHC]

#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]:
 > Yes, ok, but should this information be necessary to provide with the
 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