[GHC] #14548: Lexically scoped kind variables
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this, with `ScopedTypeVariables`: {{{ f :: forall a. Char -> Proxy (a::k) -> Int f = <body> }}} Clearly `a` scopes over `<body>`. But did you know that `k` does too? I think we'd ''expect'' `k` to scope if we wrote {{{ f :: forall (a :: K). Char -> Proxy (a::k) -> Int }}} with `k` appearing in the kind of an explicitly-forall'd binder. For long time we could not have an explicit forall for a kind variable (although we can now), so this was the ''only'' way to bring `k` into scope. But it seems altogether less desirable that an occurrence of `k` buried deep in the type should scope over `f`'s body. That's why we don't make implicitly-bound type variables scope over the body: {{{ f :: Char -> Proxy (a::k) -> Int }}} Here `a` does ''not'' scope over `<body>`. I doubt anyone would notice if we changed this behaviour, like this. * A type variable from the signature scopes over the body if * It is explicitly forall'd, or * It appears in a kind annotation of an explicitly-forall'd type variable My reason for raising this is that it's solve #14498, (by making `kk` not scope) in a uniform way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
Consider this, with `ScopedTypeVariables`: {{{ f :: forall a. Char -> Proxy (a::k) -> Int f = <body> }}} Clearly `a` scopes over `<body>`. But did you know that `k` does too?
I think we'd ''expect'' `k` to scope if we wrote {{{ f :: forall (a :: K). Char -> Proxy (a::k) -> Int }}} with `k` appearing in the kind of an explicitly-forall'd binder. For long time we could not have an explicit forall for a kind variable (although we can now), so this was the ''only'' way to bring `k` into scope.
But it seems altogether less desirable that an occurrence of `k` buried deep in the type should scope over `f`'s body. That's why we don't make implicitly-bound type variables scope over the body: {{{ f :: Char -> Proxy (a::k) -> Int }}} Here `a` does ''not'' scope over `<body>`.
I doubt anyone would notice if we changed this behaviour, like this.
* A type variable from the signature scopes over the body if * It is explicitly forall'd, or * It appears in a kind annotation of an explicitly-forall'd type variable
My reason for raising this is that it's solve #14498, (by making `kk` not scope) in a uniform way.
New description: Consider this, with `ScopedTypeVariables`: {{{ f :: forall a. Char -> Proxy (a::k) -> Int f = <body> }}} Clearly `a` scopes over `<body>`. But did you know that `k` does too? I think we'd ''expect'' `k` to scope if we wrote {{{ f :: forall (a :: K). Char -> Proxy (a::k) -> Int }}} with `k` appearing in the kind of an explicitly-forall'd binder. For long time we could not have an explicit forall for a kind variable (although we can now), so this was the ''only'' way to bring `k` into scope. But it seems altogether less desirable that an occurrence of `k` buried deep in the type should scope over `f`'s body. That's why we don't make implicitly-bound type variables scope over the body: {{{ f :: Char -> Proxy (a::k) -> Int }}} Here `a` does ''not'' scope over `<body>`. I doubt anyone would notice if we changed this behaviour, like this. * A type variable from the signature scopes over the body if * It is explicitly forall'd, or * It appears in a kind annotation of an explicitly-forall'd type variable My reason for raising this is that it's solve #14498 (by making `kk` not scope) in a uniform way. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14288, #14498 Comment: Sounds good to me. I tried implementing this at one point, but alas, the structure of `HsImplicitBndrs` does not make it easy to distinguish between a `k` appearing in `forall a. Char -> Proxy (a::k) -> Int` and a `k` appearing in `forall (a :: k). Char -> Proxy (a::k) -> Int`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I know. But before implementing anything we should agree the design. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm not sure what "design" you're talking about. I agree to the proposal in the ticket. Done. What else are we blocked on? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, that's the design. Before implementing it, though, we need to check that others are happy. Perhaps it's too much of a corner case to bother with a GHC proposal? What do others think? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
Consider this, with `ScopedTypeVariables`: {{{ f :: forall a. Char -> Proxy (a::k) -> Int f = <body> }}} Clearly `a` scopes over `<body>`. But did you know that `k` does too?
I think we'd ''expect'' `k` to scope if we wrote {{{ f :: forall (a :: K). Char -> Proxy (a::k) -> Int }}} with `k` appearing in the kind of an explicitly-forall'd binder. For long time we could not have an explicit forall for a kind variable (although we can now), so this was the ''only'' way to bring `k` into scope.
But it seems altogether less desirable that an occurrence of `k` buried deep in the type should scope over `f`'s body. That's why we don't make implicitly-bound type variables scope over the body: {{{ f :: Char -> Proxy (a::k) -> Int }}} Here `a` does ''not'' scope over `<body>`.
I doubt anyone would notice if we changed this behaviour, like this.
* A type variable from the signature scopes over the body if * It is explicitly forall'd, or * It appears in a kind annotation of an explicitly-forall'd type variable
My reason for raising this is that it's solve #14498 (by making `kk` not scope) in a uniform way.
New description: Consider this, with `ScopedTypeVariables`: {{{ f :: forall a. Char -> Proxy (a::k) -> Int f = <body> }}} Clearly `a` scopes over `<body>`. But did you know that `k` does too? I think we'd ''expect'' `k` to scope if we wrote {{{ f :: forall (a :: k). Char -> Proxy (a::k) -> Int }}} with `k` appearing in the kind of an explicitly-forall'd binder. For long time we could not have an explicit forall for a kind variable (although we can now), so this was the ''only'' way to bring `k` into scope. But it seems altogether less desirable that an occurrence of `k` buried deep in the type should scope over `f`'s body. That's why we don't make implicitly-bound type variables scope over the body: {{{ f :: Char -> Proxy (a::k) -> Int }}} Here `a` does ''not'' scope over `<body>`. I doubt anyone would notice if we changed this behaviour, like this. * A type variable from the signature scopes over the body if * It is explicitly forall'd, or * It appears in a kind annotation of an explicitly-forall'd type variable My reason for raising this is that it's solve #14498 (by making `kk` not scope) in a uniform way. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14548: Lexically scoped kind variables -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14288, #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I wouldn't expect `k` to scope over the body in either of the original examples. I think that users should have to explicitly bind `k` in the `forall` to get it to scope. However, making this not so painful will require sorting out [https://github.com/ghc-proposals/ghc-proposals/pull/83 this proposal] first. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14548#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC