Pattern synonyms don't work with GADTs
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.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.8.4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Pattern synonyms don't work with GADTs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this variant of test `T8968-1`:\r\n{{{\r\n{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}\r\nmodule ShouldCompile where\r\n\r\ndata X :: * -> * where\r\n Y :: a -> X (Maybe a)\r\n\r\npattern C :: a -> X (Maybe a)\r\npattern C x = Y x\r\n\r\nfoo :: X t -> t\r\nfoo (C x) = Just x\r\n}}}\r\n * If we had `(Y x)` instead of `(C x)` in the LHS of `foo`, then this is an ordinary GADT program and typechecks fine. \r\n\r\n * If we omit the pattern signature, it typechecks fine, and `:info C` says\r\n{{{\r\npattern C :: t ~ Maybe a => a -> X t \t-- Defined in ‘ShouldCompile’\r\n}}}\r\n\r\n * But as written, it fails with\r\n{{{\r\nFoo.hs:11:6:\r\n Couldn't match type ‘t’ with ‘Maybe a0’\r\n ‘t’ is a rigid type variable bound by\r\n the type signature for: foo :: X t -> t at Foo.hs:10:8\r\n Expected type: X t\r\n Actual type: X (Maybe a0)\r\n Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)\r\n In the pattern: C x\r\n In an equation for ‘foo’: foo (C x) = Just x\r\n}}}\r\n Moreover, `:info C` says\r\n{{{\r\npattern C :: a -> X (Maybe a) \t-- Defined at Foo.hs:8:9\r\n}}}\r\n\r\nDo you see the difference? In the former, the \"prov_theta\" equality constraint is explicit, but in the latter it's implicit.\r\n\r\nThe 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).\r\n\r\nThis is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.","type_of_failure":"OtherFailure","blocking":[]} -->
issue