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

 To clarify:

 1. In `pattern Q :: () => Eq b => Disguised a b`, `b` will be inferred to
 be universal, and the return type will be `b -> RP a`. This is slightly
 different than the original `Disguised` example from the paper, in that
 the original example suggested that the return type be `RP a`.

 2. In `pattern R :: (a -> Maybe a)`, `R` is a nullary pattern synonym,
 because the "find return type" algorithm doesn't look through parentheses.
 `pattern R a = Just a` would be rejected. `R`'s type is distinct from
 `pattern R2 :: a -> Maybe a`, which is a unary pattern synonym.

 Perhaps when describing this feature, we should be clear that the syntax
 of a pattern signature is this:
 * It has a nested structure. The top-level is a triple of things (the
 universals, the existentials, and the term-level typing information),
 separated by `=>`.
 * If no `=>` are present, then the one item is really the term-level
 typing information.
 * If one `=>` is present, then the first item is the universals, and the
 second item is the term-level typing information.
 * Both the universals and existentials have the same syntax: an optional
 `forall ...`, followed by a constraint.
 * The term-level typing information is a list of types, with at least one
 element. The list separator is spelled `->`.
 * The last type in the list is the return type. All other types (there may
 be none) are argument types.

 I've (briefly) tried to write out the BNF-style grammar here, but that's
 surprisingly challenging. For example, `forall a. blah` makes is accepted,
 but what does `forall a. forall b. blah` mean? Is `b` existential? Or do
 we need a `() =>` to make that happen?

 This is all horribly complicated!

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