
#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