[GHC] #14548: Lexically scoped kind variables

Fri Dec 1 16:05:06 UTC 2017

#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