[GHC] #12187: Clarify the scoping of existentials for pattern synonym signatures
#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 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #12108 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- What are scoping rules for type variables in pattern synonym signatures? We said that existentials variables are scoped as follows: 1. Existentials scope over only the provided constraints and the arguments, not over the result type. {{{ type Disguised a b = b -> RP a pattern Q :: () => Eq b => Disguised a b }}} However, Simon argues that `Q` should be accepted as if we expand the type synonym then the existentially quantified `b` is no longer in the result type. Richard disagrees, he considers the result type to be `Disguised a b` and so `b` is in the result type and not in-scope. Therefore he wishes to reject this example. The purpose of this ticket is to decide the fate of `Q`. This kind of problem is related to #12108 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: simonpj, goldfire (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: mpickering (added) Comment: Is every one happy with this? Richard? Matthew? Gergo? If so I'll go ahead. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Description changed by simonpj: @@ -24,1 +24,1 @@ - This kind of problem is related to #12108 + This kind of problem is related to #12108, #12179 New description: What are scoping rules for type variables in pattern synonym signatures? We said that existentials variables are scoped as follows: 1. Existentials scope over only the provided constraints and the arguments, not over the result type. {{{ type Disguised a b = b -> RP a pattern Q :: () => Eq b => Disguised a b }}} However, Simon argues that `Q` should be accepted as if we expand the type synonym then the existentially quantified `b` is no longer in the result type. Richard disagrees, he considers the result type to be `Disguised a b` and so `b` is in the result type and not in-scope. Therefore he wishes to reject this example. The purpose of this ticket is to decide the fate of `Q`. This kind of problem is related to #12108, #12179 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): And how do we reject {{{ pattern Bad :: () => forall a. T a }}} Do we follow your proposed rules and then check to make sure that there are no existentials in the (expanded) return type? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): There should be no existentials in the return type. So that type signature would be rejected with that message. I'll edit comment:3 to clarify that Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 don't think it's complicated. {{{ qualifier ::= forall tv1 .. tvn. | forall tv1 .. tvn. ctxt => | ctxt => body ::= btype -> body | type -- without an arrow at the top pat_ty ::= qualifier qualifier body -- Univ and ext | qualifier body -- Univ only | body }}} A qualifier has a `forall` or `=>` or both. A pattern type has zero, one, or two qualifiers. Needless to say I'm open to better ideas. But we need SOME way to specify it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12187#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC