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

 OK. Now I understand what you're doing better. Here is how I see it:

 1. The renamer really shouldn't bring any of the existentials into scope,
 as existentials in a pattern synonym type don't scope over the (entire)
 pattern synonym body.

 2. But the renamer can't tell existential implicitly bound variables from
 universal ones.

 3. So, the renamer brings into scope only the universals and all the
 implicitly bound ones. This brings more variables into scope than it
 should.

 4. The pattern synonym body then is renamed with some extra variables in
 scope, so more uniques match between the body and the type than morally
 should. In addition, less implicit quantification happens in the body than
 morally should.

 5. The type-checker must deal with this unfolding disaster by duplicating
 the renamer's strange behavior: it brings into scope implicitly-bound
 existentials, just so that weird out-of-scope errors don't happen in the
 body. But it arranges to error if these are encountered, regardless.

 6. The program in this ticket observes that the difference in treatment
 between implicitly bound and explicitly bound is awkward.

 7. Your proposed solution is just to bring all existentials into scope in
 both the renamer and the type-checker, so that treatment is uniform. This
 is done even though existentials really shouldn't scope over the body.

 8. This ticket is all about uniformity. The behavior in both the explicit
 case and the implicit case is, by itself, correct. But it's awkward for
 GHC's behavior to depend on the user's choice of implicit vs explicit
 binding.

 Is that a fair assessment?

 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.

 And, the patch as written actually makes GHC's behavior worse, in that
 it's further from the ideal of "existentials do not scope". The only
 reason to do this patch is that we cannot achieve the ideal, and this
 patch does indeed (and correctly, as far as I can tell) make the behavior
 more uniform.

 So I do think the best way to fix this problem is to ignore it and wait
 for it to go away. :)

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