Currently there is a lot of code duplication in the way Typeable is implemented (Section 7.5.3, “Deriving clause for extra classes (Typeable, Data, etc)”):

class Typeable (t :: *) where
  typeOf :: t -> TypeRep

class Typeable1 (t :: * -> *) where
  typeOf1 :: t a -> TypeRep

class Typeable2 (t :: * -> * -> *) where
  typeOf2 :: t a b -> TypeRep

Kind polymorphism (with -XPolyKinds) allows us to merge all these classes into one:

data Proxy t = Proxy

class Typeable t where
  typeOf :: Proxy t -> TypeRep

instance Typeable Int  where typeOf _ = TypeRep
instance Typeable []   where typeOf _ = TypeRep

Note that the datatype Proxy has kind forall k. k -> * (inferred by GHC), and the new Typeable class has kind forall k. k -> Constraint.

Generally speaking, with -XPolyKinds, GHC will infer a polymorphic kind for un-decorated declarations, whenever possible. For example:

data T m a = MkT (m a)
-- GHC infers kind   T :: forall k. (k -> *) -> k -> *

Just as in the world of terms, you can restrict polymorphism using a kind signature (sometimes called a kind annotation) (-XPolyKinds implies -XKindSignatures):

data T m (a :: *) = MkT (m a)
-- GHC now infers kind   T :: (* -> *) -> * -> *

There is no "forall" for kind variables. Instead, when binding a type variable, you can simply mention a kind variable in a kind annotation for that type-variable binding, thus:

data T (m :: k -> *) a = MkT (m a)
-- GHC now infers kind   T :: forall k. (k -> *) -> k -> *

The kind "forall" is placed just outside the outermost type-variable binding whose kind annotation mentions the kind variable. For example

f1 :: (forall a m. m a -> Int) -> Int
         -- f1 :: forall (k:BOX).
         --       (forall (a:k) (m:k->*). m a -> Int)
         --       -> Int

f2 :: (forall (a::k) m. m a -> Int) -> Int
         -- f2 :: (forall (k:BOX) (a:k) (m:k->*). m a -> Int)
         --       -> Int

Here in f1 there is no kind annotation mentioning the polymorphic kind variable, so k is generalised at the top level of the signature for f1, making the signature for f1 is as polymorphic as possible. But in the case of of f2 we give a kind annotation in the forall (a:k) binding, and GHC therefore puts the kind forall right there too.

(Note: These rules are a bit indirect and clumsy. Perhaps GHC should allow explicit kind quantification. But the implicit quantification (e.g. in the declaration for data type T above) is certainly very convenient, and it is not clear what the syntax for explicit quantification should be.)

Just as in type inference, kind inference for recursive types can only use monomorphic recursion. Consider this (contrived) example:

data T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind  T :: (* -> *) -> * -> *

The recursive use of T forced the second argument to have kind *. However, just as in type inference, you can achieve polymorphic recursion by giving a complete kind signature for T. The way to give a complete kind signature for a data type is to use a GADT-style declaration with an explicit kind signature thus:

data T :: (k -> *) -> k -> * where
  MkT :: m a -> T Maybe (m a) -> T m a

The complete user-supplied kind signature specifies the polymorphic kind for T, and this signature is used for all the calls to T including the recursive ones. In particular, the recursive use of T is at kind *.

What exactly is considered to be a "complete user-supplied kind signature" for a type constructor? These are the forms:

In a complete user-specified kind signature, any un-decorated type variable to the left of the "::" is considered to have kind "*". If you want kind polymorphism, specify a kind variable.

Although all open type families are considered to have a complete user-specified kind signature, we can relax this condition for closed type families, where we have equations on which to perform kind inference. GHC will infer a kind for any type variable in a closed type family when that kind is never used in pattern-matching. If you want a kind variable to be used in pattern-matching, you must declare it explicitly.

Here are some examples (assuming -XDataKinds is enabled):

type family Not a where      -- Not :: Bool -> Bool
  Not False = True
  Not True  = False

type family F a where        -- ERROR: requires pattern-matching on a kind variable
  F Int   = Bool
  F Maybe = Char

type family G (a :: k) where -- G :: k -> *
  G Int   = Bool
  G Maybe = Char

type family SafeHead where   -- SafeHead :: [k] -> Maybe k
  SafeHead '[] = Nothing     -- note that k is not required for pattern-matching
  SafeHead (h ': t) = Just h

Consider the following example of a poly-kinded class and an instance for it:

class C a where
  type F a

instance C b where
  type F b = b -> b

In the class declaration, nothing constrains the kind of the type a, so it becomes a poly-kinded type variable (a :: k). Yet, in the instance declaration, the right-hand side of the associated type instance b -> b says that b must be of kind *. GHC could theoretically propagate this information back into the instance head, and make that instance declaration apply only to type of kind *, as opposed to types of any kind. However, GHC does not do this.

In short: GHC does not propagate kind information from the members of a class instance declaration into the instance declaration head.

This lack of kind inference is simply an engineering problem within GHC, but getting it to work would make a substantial change to the inference infrastructure, and it's not clear the payoff is worth it. If you want to restrict b's kind in the instance above, just use a kind signature in the instance head.