Consider this variant of test T8968-1:

{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where

data X :: * -> * where
  Y :: a -> X (Maybe a)

pattern C :: a -> X (Maybe a)
pattern C x = Y x

foo :: X t -> t
foo (C x) = Just x

• If we had (Y x) instead of (C x) in the LHS of foo, then this is an ordinary GADT program and typechecks fine.
• If we omit the pattern signature, it typechecks fine, and :info C says

pattern C :: t ~ Maybe a => a -> X t 	-- Defined in ‘ShouldCompile’

• But as written, it fails with

Foo.hs:11:6:
    Couldn't match type ‘t’ with ‘Maybe a0’
      ‘t’ is a rigid type variable bound by
          the type signature for: foo :: X t -> t at Foo.hs:10:8
    Expected type: X t
      Actual type: X (Maybe a0)
    Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
    In the pattern: C x
    In an equation for ‘foo’: foo (C x) = Just x

Moreover, :info C says

pattern C :: a -> X (Maybe a) 	-- Defined at Foo.hs:8:9

Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit.

The exact thing happens for DataCons. It's handled via the dcEqSpec field. Essentially PatSyn should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in TcTyClsDecls.rejigConRes (perhaps needs a better name).

This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.