[GHC] #14548: Lexically scoped kind variables

Fri Dec 1 11:41:19 UTC 2017

#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