Note [Inferring kinds for type declarations]

This note deals with /inference/ for type declarations
that do not have a CUSK or a SAKS.  Consider
  data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x)
  data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y)

We do kind inference as follows:

* Step 1: inferInitialKinds, and in particular kcInferDeclHeader.
  Make a unification variable for each of the Required and Specified
  type variables in the header.

  Record the connection between the Names the user wrote and the
  fresh unification variables in the tcTyConScopedTyVars field
  of the TcTyCon we are making
      [ (a,  aa)
      , (k1, kk1)
      , (k2, kk2)
      , (x,  xx) ]
  (I'm using the convention that double letter like 'aa' or 'kk'
  mean a unification variable.)

  These unification variables
    - Are TyVarTvs: that is, unification variables that can
      unify only with other type variables.
      See Note [TyVarTv] in GHC.Tc.Utils.TcMType

    - Have complete fresh Names; see GHC.Tc.Utils.TcMType
      Note [Unification variables need fresh Names]

  Assign initial monomorphic kinds to S, T
          T :: kk1 -> * -> kk2 -> *
          S :: kk3 -> * -> kk4 -> *

* Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
  T, with these monomorphic kinds.  Now kind-check the declarations,
  and solve the resulting equalities.  The goal here is to discover
  constraints on all these unification variables.

  Here we find that kk1 := kk3, and kk2 := kk4.

  This is why we can't use skolems for kk1 etc; they have to
  unify with each other.

* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
  We find the free variables of the kind, skolemise them,
  sort them out into Inferred/Required/Specified (see the above
  Note [Required, Specified, and Inferred for types]),
  and perform some validity checks.

  This makes the utterly-final TyConBinders for the TyCon.

  All this is very similar at the level of terms: see GHC.Tc.Gen.Bind
  Note [Quantified variables in partial type signatures]

  But there are some tricky corners: Note [Tricky scoping in generaliseTcTyCon]

* Step 4.  Extend the type environment with a TcTyCon for S and T, now
  with their utterly-final polymorphic kinds (needed for recursive
  occurrences of S, T).  Now typecheck the declarations, and build the
  final AlgTyCon for S and T resp.

The first three steps are in kcTyClGroup; the fourth is in
tcTyClDecls.

There are some wrinkles

* Do not default TyVarTvs.  We always want to kind-generalise over
  TyVarTvs, and /not/ default them to Type. By definition a TyVarTv is
  not allowed to unify with a type; it must stand for a type
  variable. Hence the check in GHC.Tc.Solver.defaultTyVarTcS, and
  GHC.Tc.Utils.TcMType.defaultTyVar.  Here's another example (#14555):
     data Exp :: [TYPE rep] -> TYPE rep -> Type where
        Lam :: Exp (a:xs) b -> Exp xs (a -> b)
  We want to kind-generalise over the 'rep' variable.
  #14563 is another example.

* Duplicate type variables. Consider #11203
    data SameKind :: k -> k -> *
    data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
  Here we will unify k1 with k2, but this time doing so is an error,
  because k1 and k2 are bound in the same declaration.

  We spot this during validity checking (checkForDuplicateScopeTyVars),
  in generaliseTcTyCon.

* Required arguments.  Even the Required arguments should be made
  into TyVarTvs, not skolems.  Consider
    data T k (a :: k)
  Here, k is a Required, dependent variable. For uniformity, it is helpful
  to have k be a TyVarTv, in parallel with other dependent variables.

* Duplicate skolemisation is expected.  When generalising in Step 3,
  we may find that one of the variables we want to quantify has
  already been skolemised.  For example, suppose we have already
  generalise S. When we come to T we'll find that kk1 (now the same as
  kk3) has already been skolemised.

  That's fine -- but it means that
    a) when collecting quantification candidates, in
       candidateQTyVarsOfKind, we must collect skolems
    b) quantifyTyVars should be a no-op on such a skolem