[GHC] #12187: Clarify the scoping of existentials for pattern synonym signatures

[GHC]

#12187: Clarify the scoping of existentials for pattern synonym signatures
-------------------------------------+-------------------------------------
        Reporter:  mpickering        |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12108            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I propose the following:

 * The universal type variables are the ones free in
   * any explicitly-forall'd universal variables
   * the required context (if any)
   * the result type, after deleting any explicitly-forall'd existentials.

 * For this purpose the "result type" is very narrowly interpreted, as
 follows: first drop the required and provided contexts, if present.  Now
 drop arrows (only).  What's left is the result type.  In this suggestion,
 even parentheses stop the "dropping arrows" bit.  For example:
 {{{
 pattern X :: a -> (b -> T a)
 }}}
   Here the "result type" is `(b -> T a)`.

 * The existentials are all the rest


 This rule is simple and predictable. For `Q` in the description, both `a`
 and `b` are universal, because the result type is `Disguised a b` and both
 `a` and `b` are free.

 Moreover, you can always override it by using explicit foralls, to get
 what you want.  E.g.
 {{{
 pattern Q :: () => forall b. Eq b => Disguised a b
 }}}
 The `forall` means that `b` is no longer free in the result type

 Yes we could "look through" parens.  Yes, we could "look through" type
 synonyms, although that is harder because scopging is determined in the
 renamer.  But it's a slippery slope; e.g. what about type functions?   I
 say keep it simple.

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