[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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:5 goldfire]:
 > If so, I advocate: do nothing. This problem goes away when type
 variables and kind variables are treated identically, because if the user
 writes a `forall`, they will have to bind the kind variables explicitly
 anyway. If the user does not write a `forall`, then no scoping of type
 variables happens, so there's no problem here.

 You lost me here. The problem is that if you write out the kind variable
 in the original program explicitly:

 {{{#!hs
 pattern P :: forall. () => forall k (a :: k). Proxy a -> T
 pattern P x = MkT (x :: Proxy (a :: k))
 }}}

 Then GHC //accepts// it, contrary to the claims of `Note [Pattern synonym
 existentials do not scope]`. So no, this problem won't go away when type
 and kind variables are treated identically. (In fact, int-index had to
 specifically mark this test case as `expect_broken` in his
 [https://gitlab.haskell.org/ghc/ghc/merge_requests/361 patch] to implement
 the type-kind-variable merger.)

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