Design of Kind Polymorphism
Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker.
In types
Rules:

When there is an explicit
forall
, we don't add any foralls, which means: no implicit foralls even for kind variables
 no kind generalization, which means defaulting flexi meta kind variables to
*

A kind variable mentioned explicitly in a type must always be bound by an explicit
forall
, unlike type variables for which Haskell adds an implicitforall
. 
When there is no explicit
forall
, we add an implicit forall for notinscope type variables in the renamer, and we kind generalize in the type checker. 
In the context of a function signature, an explicit forall binds its variables (type or kind) in the function equations (as it is currently the case for type variables).
 For the following examples, no type or kind variables are in scope
f1 :: f a > Int  forall k (f :: k > *) (a :: k). f a > Int
f2 :: f (a :: k) > Int  Not in scope: kind variable `k'
f3 :: forall a. f a > Int  Not in scope: type variable `f'
f4 :: forall f a. f a > Int  forall (f :: * > *) (a :: *). f a > Int
f5 :: forall f (a :: k). f a > Int  Not in scope: kind variable `k'
 We are a little unsure about this. Mabye we
 should kindgeneralise
f6 :: forall k f a. f a > Int  Warning: Unused quantified type variable `k'
 forall k (f :: * > *) (a :: *). f a > Int
f7 :: forall k f (a :: k). f a > Int  forall k (f :: k > *) (a :: k). f a > Int
f8 :: forall k. forall f (a :: k). f a > Int  forall k (f :: k > *) (a :: k). f a > Int
g1 :: (f a > Int) > Int  forall (f :: k > *) (a :: k). (f a > Int) > Int
g2 :: (forall f a. f a > Int) > Int  forall k. (forall (f :: k > *) (a :: k). f a > Int) > Int
g3 :: (forall a. f a > Int) > Int  forall k (f :: k > *). (forall (a :: k). f a > Int) > Int
g4 :: forall f. (forall a. f a > Int) > Int  forall (f :: * > *). (forall (a :: *). f a > Int) > Int
g5 :: (forall f (a :: k). f a > Int) > Int  Not in scope: kind variable `k'
h :: forall k f (a :: k). f a > Int
h x = ...k...f a...  k, f, and a are in scope
In kinds
Rules:
 Any explicit kind variables are generalized over
 We kind generalize flexi meta kind variables when possible
We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. Only type classes have large scoping.
Type classes
Additionnal rules:
 Large scoping: any type or kind variables appearing on left or right side of a
::
in the signature is brought into scope
class C1 (f :: k1 > *) (g :: k2 > k1) where  forall k1 k2. (k1 > *) > (k2 > k1) > Constraint
foo1 :: f (g a) > (f :: k1 > *) b  forall (a :: k2) (b :: k1). f (g a) > f b
 Note that k1 and k2 scope over the type signatures
 just as f and g do.
class C2 f g where  Same as C1
foo2 :: f (g a) > f b  Same as foo1
class C3 (f :: k1 > *) g where  Same as C1
foo3 :: f (g a) > f b  Same as foo1
Data types
data T1 s as where  forall k. (k > *) > [k] > *
Foo1 :: s a > T1 s as > T1 s (a ': as)  forall k (s :: k > *) (a :: k) (as :: [k]).
 s a > T1 k s as > T1 k s ((':) k a as)
 Note that s,a do not scope over the declaration of Foo1
data T2 s (as :: [k]) where  Same as T1
Foo2 : s a > T1 s as > T1 s (a ': as)  Same as Foo1
 Note that s,as,k do not scope over the declaration of Foo2
data T3 s (as :: [*]) where  (* > *) > [*] > *
Foo3 : s a > T1 s as > T1 s (a ': as)  forall (s :: * > *) (a :: *) (as :: [*]).
 s a > T1 s as > T1 s ((':) * a as)
 Note that s,as do not scope over the declaration of Foo2
Type families
Last rule becomes: Any missing kind signature defaults to *
 Note (nothing to do with kind polymorphism) that we might want to say that only the Bool is an index.
type family F1 (b :: Bool) (true :: k) (false :: k) :: k  F1 :: forall k. Bool > k > k > k
type family F2 b true false  F2 :: * > * > * > *
type family F3 b (true :: k) false  F3 :: forall k. * > k > * > *
For type families it just doesn't make any sense to not write the whole kind signature, since there is no inference at all.
Type synonyms
type S1 f g  forall k1 k2. (k1 > *) > (k2 > k1) > *
= forall a. f (g a)  = forall (a :: k2). f (g a)
type S2 (f :: k1 > *) g  Same as S1
= forall a. f (g a)  Same as S1
type S3 (f :: k1 > *) (g :: k2 > k1)  Same as S1
= forall a. f (g a)  Same as S1
type S4 f (g :: * > *)  (* > *) > (* > *) > *
= forall a. f (g a)  = forall (a :: *). f (g a)