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

 > I think that is roughly right, yes.  But the pattern type you give above
 gives no clue that type refinement takes place when you match on it, and a
 client of `C` definitely needs to know that.

 That's why I proposed to show both types, but ...

 > I think we can print the type of `C` and `MkT` like this:
 > {{{
 > GHCi> :t MkT
 > MkT :: (b~Bool) => a -> T a b
 >
 > GHCi> :t C
 > C :: (a~Int) => Int -> X Maybe a
 >
 > GHCi> pattern D x = MkT (Just x)
 > GHCi> :t D
 > D :: (b~Bool) => a -> T (Maybe a) b
 > }}}
 > These types work nicely both in expressions and patterns.

 Yes, I'm certainly happy with this as well. In fact, I had briefly
 considered making this suggestion. (I think back in GHC 6, GADT
 constructor types were actually displayed using a similar syntax.) My only
 worry is that it's slightly subtle that in these cases
 (where it's a type signature for a constructor or pattern synonym),
 inlining an equality
 constraint makes a difference, whereas for expressions it doesn't. But I
 guess that
 having two different type signatures printed wouldn't be any easier to
 understand.

 > The pattern synonym D is a nice example:
 >  * The result type `T (Maybe a) b` says that `D` must only match types
 of that shape, i.e. where the first arg of `T` is a `Maybe`.
 >  * The `(b~Bool) =>` says that when you match on `D` you get that type
 refinement available in the case alternative.
 >
 > So this actually a single signature that tells you all you need to know,
 both for matching and for use in expressions.  Good!

 Yes, ok.

 > I should mention that internally the type of a GADT constructor like
 `MkT` really is as displayed here, namely `MkT :: (b~Bool) => a -> T a b`.

 Also good.

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