Alas, no. If the definition of T really did have that constructor P,
#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): then GADT-style type refinement would take place when you match on P. So for example, this would typecheck:
{{{ f :: T a b -> a -> Bool f P v = v && True }}} But obviously the expansion does not: {{{ f :: T a b -> a -> Bool f (MkT x) v = v && True }}}
The expansion is `MkT True`, but it doesn't matter. Nice example. I'm almost convinced, although I'll have to think about this a bit longer.
Moreover, these are terribly simple examples. In general a pattern synonym might mention dozens of constructor from dozens of types. Which of those types would you like to pretend the pattern synonym constructor is from?
I don't pretend that I have thought this through. I have only played with pattern synonyms for a few days so far, and I don't completely understand the possibilities of the interaction with ViewPatterns yet. However, in the case of bidirectional pattern synonyms I'd expect a pattern synonym to have a clear "target type".
This is what I mean by modularity: no matter how complicated the right hand side of the pattern synonym, I want the client (of the library defining the pattern synonym) to be able to use it by knowing only its type -- just like he can for a function exported by a library.
Yes, that's certainly a valid goal. Ok, for now, let's try to summarize: Every (bidirectional) pattern actually has two types, an "expression type" and a "pattern type". If I understand your proposal correctly, you're saying that pattern type signatures should allow the user specify the pattern type, because the expression type should in general be easy to infer. So I should be able to say {{{ pattern P :: T Bool b pattern P = MkT True }}} or for my original example {{{ pattern C :: Int -> Maybe a pattern C x = Y (Just x) }}} So perhaps GHCi should print both types rather than only the expression type on `:t`, something like: {{{ GHCi> :t C pattern C :: Int -> Maybe a C :: Int -> Maybe Int GHCi> :t P pattern P :: T Bool b P :: T Bool Bool }}} And perhaps for consistency even for normal data constructors? {{{ GHCi> :t MkT pattern MkT :: a -> T a b MkT :: a -> T a Bool }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler