Skip to content

Lexically scoped kind variables

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 (closed) (by making kk not scope) in a uniform way.

Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information