[GHC] #8968: Pattern synonyms and GADTs

[GHC]

#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