[GHC] #16315: Pattern synonym implicit existential quantification

[GHC]

#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
           Reporter:  int-index      |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

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