[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     |           Version:  7.8.1-rc2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 I think this one is different from #8966, but feel free to close one as
 duplicate if it turns out to be the same problem.

 The following program (using GADTs and pattern synonyms, but not kind
 polymorphism or data kinds) fails to check with ghc-7.8.1-rc2, but I think
 it should:
 {{{
 {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}

 data X :: (* -> *) -> * -> * where
   Y :: f Int -> X f Int

 pattern C x = Y (Just x)
 }}}
 The error I get is the following:
 {{{
 PatKind.hs:6:18:
     Couldn't match type ‘t’ with ‘Maybe’
       ‘t’ is untouchable
         inside the constraints (t1 ~ Int)
         bound by a pattern with constructor
                    Y :: forall (f :: * -> *). f Int -> X f Int,
                  in a pattern synonym declaration
         at PatKind.hs:6:15-24
       ‘t’ is a rigid type variable bound by
           the inferred type of
           C :: X t t1
           x :: Int
           at PatKind.hs:1:1
     Expected type: t Int
       Actual type: Maybe Int
     In the pattern: Just x
     In the pattern: Y (Just x)

 PatKind.hs:6:18:
     Could not deduce (t ~ Maybe)
     from the context (t1 ~ Int)
       bound by the type signature for
                  (Main.$WC) :: t1 ~ Int => Int -> X t t1
       at PatKind.hs:6:9
       ‘t’ is a rigid type variable bound by
           the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1
           at PatKind.hs:1:1
     Expected type: t Int
       Actual type: Maybe Int
     Relevant bindings include
       ($WC) :: Int -> X t t1 (bound at PatKind.hs:6:9)
     In the first argument of ‘Y’, namely ‘(Just x)’
     In the expression: Y (Just x)
 }}}

 Note that I'd be perfectly happy to provide a type signature for the
 pattern synonym, but I don't know of any syntax I could use. The Wiki page
 at https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms mentions I might
 be able to write
 {{{
 pattern C :: Int -> X Maybe Int
 }}}
 but this triggers a parse error.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8968>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler