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 simonpj): Replying to [comment:6 kosmikus]: 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`. But '''not''' in a pattern context, otherwise this function would be ill- typed: {{{ 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, they can soundly (without seg-faulting) match any value of type `T <type>`. So `f :: T a -> Bool`. But try this: {{{ g (T1 True) = True g T2 = True g T3 = False }}} Here the first equation means that applying `g` to an argument of type `T Int`, say, would be unsound. The pattern `T1 True :: T Bool`, and indeed `g :: T Bool -> Bool`, and the `T2` clause is dead code. 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. However, a key principle is that replacing pattern synonym by its definition should not change whether the program is well typed. So is is a bug that these two behave differently: {{{ f :: X Maybe a -> a f (Y (Just x)) = x -- works f (C x) = x -- fails }}} The latter should not fail; it should behave precisely like the former. The "not in scope during type checking" error is a bug. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler