#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): 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. 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 -> 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. * In expressions they are precisely equivalent to `a -> T a Bool` and `Int -> Maybe Int` respectively. * In patterns, pattern matching binds evidence for the equality. In Gergo's terminology, matching against `MkT` "provides" `(b~Bool)`; this refinement is available in the case alternative. 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! (There is a twist for what Gergo calls "required" constraints, which arise in view patterns and literal patterns, but let's ignore that for now.) Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler