[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):

 OK. If I understand you correctly, then the original program with `k`
 uncommented should be accepted. (I think you were hinting at this all
 along, but it wasn't obvious to me until comment:7.) If that's the case,
 then it sounds like the proper course of action is to:

 * Proceed with https://gitlab.haskell.org/ghc/ghc/merge_requests/374, as
 it will get rid of the awkwardness brought about by implicitly quantified
 variables being brought into scope.
 * Moreover, !374 can revert most of #14998:
   * There is no longer any need for `PatSynExPE`, since implicitly
 quantified existentials are no longer brought into scope.
   * `Note [Pattern synonym existentials do not scope]` can go away.
   * The `T14498` test case can be removed. (Or, alternatively, we could
 explicitly quantify `k` and move it to `patsyn/should_compile`.)

 Does this sound right?

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