Note [Recipe for checking a signature]

Kind-checking a user-written signature requires several steps:

 0. Bump the TcLevel
 1.   Bind any lexically-scoped type variables.
 2.   Generate constraints.
 3. Solve constraints.
 4. Sort any implicitly-bound variables into dependency order
 5. Promote tyvars and/or kind-generalize.
 6. Zonk.
 7. Check validity.

Very similar steps also apply when kind-checking a type or class
declaration.

The general pattern looks something like this.  (But NB every
specific instance varies in one way or another!)

    do { (tclvl, wanted, (spec_tkvs, ty))
              <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
                 bindImplicitTKBndrs_Skol sig_vars              $
                 <kind-check the type>

       ; spec_tkvs <- zonkAndScopedSort spec_tkvs

       ; reportUnsolvedEqualities skol_info spec_tkvs tclvl wanted

       ; let ty1 = mkSpecForAllTys spec_tkvs ty
       ; kvs <- kindGeneralizeAll ty1

       ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)

       ; checkValidType final_ty

This pattern is repeated many times in GHC.Tc.Gen.HsType,
GHC.Tc.Gen.Sig, and GHC.Tc.TyCl, with variations.  In more detail:

* pushLevelAndSolveEqualitiesX (Step 0, step 3) bumps the TcLevel,
  calls the thing inside to generate constraints, solves those
  constraints as much as possible, returning the residual unsolved
  constraints in 'wanted'.

* bindImplicitTKBndrs_Skol (Step 1) binds the user-specified type
  variables E.g.  when kind-checking f :: forall a. F a -> a we must
  bring 'a' into scope before kind-checking (F a -> a)

* zonkAndScopedSort (Step 4) puts those user-specified variables in
  the dependency order.  (For "implicit" variables the order is no
  user-specified.  E.g.  forall (a::k1) (b::k2). blah k1 and k2 are
  implicitly brought into scope.

* reportUnsolvedEqualities (Step 3 continued) reports any unsolved
  equalities, carefully wrapping them in an implication that binds the
  skolems.  We can't do that in pushLevelAndSolveEqualitiesX because
  that function doesn't have access to the skolems.

* kindGeneralize (Step 5). See Note [Kind generalisation]

* The final zonkTcTypeToType must happen after promoting/generalizing,
  because promoting and generalizing fill in metavariables.


Doing Step 3 (constraint solving) eagerly (rather than building an
implication constraint and solving later) is necessary for several
reasons:

* Exactly as for Solver.simplifyInfer: when generalising, we solve all
  the constraints we can so that we don't have to quantify over them
  or, since we don't quantify over constraints in kinds, float them
  and inhibit generalisation.

* Most signatures also bring implicitly quantified variables into
  scope, and solving is necessary to get these in the right order
  (Step 4) see Note [Keeping implicitly quantified variables in
  order]).