#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