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.