
#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