Replying to [comment:6 kosmikus]:
Both `P` in SPJ's example and `C` in my examples are bidirectional
#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]: 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`.
{{{ 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,
But '''not''' in a pattern context, otherwise this function would be ill- typed: 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