Pattern synonym implicit existential quantification
This code typechecks when `k` is brought into scope explicitly, but not implicitly (code example courtesy of RyanGlScott):
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Kind
import Data.Proxy
data T = forall k (a :: k). MkT (Proxy a)
-- Uncomment `k` and it typechecks
pattern P :: forall. () => forall {-k-} (a :: k). Proxy a -> T
pattern P x = MkT (x :: Proxy (a :: k))
```
I discovered this because I was implementing https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst and had to explicitly quantify some definitions in the test suite. Then the test case for #14498 stopped producing the error that it should.
It seems indicative of an issue in typechecking pattern synonyms: I would expect equal treatment for implicit and explicit type/kind variables.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | RyanGlScott |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Pattern synonym implicit existential quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott"],"type":"Bug","description":"This code typechecks when `k` is brought into scope explicitly, but not implicitly (code example courtesy of RyanGlScott):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata T = forall k (a :: k). MkT (Proxy a)\r\n\r\n-- Uncomment `k` and it typechecks\r\npattern P :: forall. () => forall {-k-} (a :: k). Proxy a -> T\r\npattern P x = MkT (x :: Proxy (a :: k))\r\n}}}\r\n\r\nI discovered this because I was implementing https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst and had to explicitly quantify some definitions in the test suite. Then the test case for #14498 stopped producing the error that it should.\r\n\r\nIt seems indicative of an issue in typechecking pattern synonyms: I would expect equal treatment for implicit and explicit type/kind variables.","type_of_failure":"OtherFailure","blocking":[]} -->
issue