[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:6 kosmikus]:
 > Both `P` in SPJ's example and `C` in my examples are bidirectional
 pattern synonyms, and as an expression, it should be easy enough for GHC
 to type-check without a type signature. So why require one in this case?
 The expression type signature and pattern type signature must be the same,
 after all.

 No, that statement sounds plausible, but it is not right.  Consider
 {{{
 data T a where
   T1 :: a -> T a
   T2 :: T Int
   T3 :: T Bool
 }}}
 In an expression context, certainly, `T2 :: T Int`, and `T3 :: T Bool`.
 But '''not''' in a pattern context, otherwise this function would be ill-
 typed:
 {{{
 f (T1 _) = True
 f T2 = True
 f T3 = False
 }}}
 No, as a pattern, both `T2` and `T3` have type `forall a. T a`; that is,
 they can soundly (without seg-faulting) match any value of type `T
 <type>`.  So `f :: T a -> Bool`.

 But try this:
 {{{
 g (T1 True) = True
 g T2 = True
 g T3 = False
 }}}
 Here the first equation means that applying `g` to an argument of type `T
 Int`, say, would be unsound.  The pattern `T1 True :: T Bool`, and indeed
 `g :: T Bool -> Bool`, and the `T2` clause is dead code.

 The trouble is that (as we know well) in the presence of GADTs there may
 be no unique principal type, which is why !OutsideIn requires type
 signatures to resolve the uncertainty.  It's the same with pattern
 synonyms.

 However, a key principle is that replacing pattern synonym by its
 definition should not change whether the program is well typed.  So is is
 a bug that these two behave differently:
 {{{
 f :: X Maybe a -> a
 f (Y (Just x)) = x      -- works
 f (C x) = x             -- fails
 }}}
 The latter should not fail; it should behave precisely like the former.

 The "not in scope during type checking" error is a bug.

 Simon

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