#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): After thinking about this some more, I'm getting more confused. How should pattern matching on these pattern synonyms work? Both `P` in SPJ's example and `C` in my examples are bidirectional 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. (Even for unidirectional ones, I'd argue that probably inferring a type for the pattern itself shouldn't be too difficult.) The main question is whether such synonyms can then be used in order to trigger type refinement. It currently seems they cannot, no matter what type they have. For my original example, consider this: {{{ {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f Int -> X f Int pattern C x = Y (Just x) :: X Maybe Int f :: X Maybe a -> a f (Y (Just x)) = x -- works f (C x) = x -- fails }}} For Simon's example, consider: {{{ {-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, RankNTypes #-} data T a b where MkT :: a -> T a Bool MkX :: T a b Q1 :: T Bool Bool Q2 :: T Bool b Q3 :: T b Bool Q4 :: T b b pattern P1 = MkT True :: T Bool Bool pattern P1a <- MkT True :: T Bool Bool pattern P2a <- MkT True :: forall b. T Bool b pattern P3a <- MkT True :: forall b. T b Bool pattern P4a <- MkT True :: forall b. T b b f :: T Bool b -> Bool f (MkT True) = True -- works f Q1 = True -- works f Q2 = undefined -- works f Q3 = True -- works f Q4 = True -- works f P1 = True -- fails f P1a = True -- fails f P2a = undefined -- fails f P3a = True -- fails f P4a = True -- fails }}} Is it unreasonable to expect this kind of thing to work? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler