[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 kosmikus):

 Replying to [comment:7 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`.

 Ok, we seem to have slightly different terminology when it comes to saying
 what the "type" of a pattern is. But terminology aside, I agree that `T2`
 and `T3` should be applicable in a context of type `T a`. But the
 information that they're `T Int` and `T Bool` "as an expression" must
 still be around even during pattern matching, because the match causes
 type refinement accordingly.

 So in one way or another for a constructor such as `T2` there seem to be
 *two* types that are important, namely `T Int` and `forall a. T a`.

 > 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.

 This is what I also thought at first, but what I'm no longer convinced
 about.

 Let's go back to your example:
 {{{
 data T a b where
         MkT :: a -> T a Bool
         MkX :: T a b

 pattern P = MkT True
 }}}

 So I guess we agree than "as an expression", `P` must be of type `T Bool
 Bool`. You say that "as a pattern", it could have either of
 {{{
 P :: T Bool b
 P :: T b b
 }}}
 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?

 Shouldn't I be able to write
 {{{
 f :: T Bool b -> b
 f P = False
 }}}
 and also
 {{{
 g :: T b b -> b
 g P = False
 }}}
 just like I can write
 {{{
 f :: T Bool b -> b
 f (MkT True) = False
 }}}
 as well as
 {{{
 g :: T b b -> b
 g (MkT True) = False
 }}}

 If I'd be forced to provide a type signature for the pattern synonym `P`
 picking one of the two "pattern types", then `P` would be necessarily more
 limited in its use than its expansion.

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