Pattern synonyms and GADTs

I think this one is different from #8966 (closed), 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.

Trac metadata

Trac field	Value
Version	7.8.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture