Note [Using TyVarTvs for kind-checking GADTs]

Consider

  data Proxy a where
    MkProxy1 :: forall k (b :: k). Proxy b
    MkProxy2 :: forall j (c :: j). Proxy c

It seems reasonable that this should be accepted. But something very strange
is going on here: when we're kind-checking this declaration, we need to unify
the kind of `a` with k and j -- even though k and j's scopes are local to the type of
MkProxy{1,2}.

In effect, we are simply gathering constraints on the shape of Proxy's
kind, with no skolemisation or implication constraints involved at all.

The best approach we've come up with is to use TyVarTvs during the
kind-checking pass, rather than ordinary skolems. This is why we use
the "_Tv" variant, bindOuterSigTKBndrs_Tv.

Our only goal is to gather constraints on the kind of the type constructor;
we do not certify that the data declaration is well-kinded. For example:

  data SameKind :: k -> k -> Type
  data Bad a where
    MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)

which would be accepted by kcConDecl because k1 and k2 are
TyVarTvs. It is correctly rejected in the second pass, tcConDecl.
(Test case: polykinds/TyVarTvKinds3)

One drawback of this approach is sometimes it will accept a definition that
a (hypothetical) declarative specification would likely reject. As a general
rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs
approach allows a limited form of polymorphic recursion *without* a CUSK.

To wit:
  data T a = forall k (b :: k). MkT (T b) Int
  (test case: dependent/should_compile/T14066a)

Note that this is polymorphically recursive, with the recursive occurrence
of T used at a kind other than a's kind. The approach outlined here accepts
this definition, because this kind is still a kind variable (and so the
TyVarTvs unify). Stepping back, I (Richard) have a hard time envisioning a
way to describe exactly what declarations will be accepted and which will
be rejected (without a CUSK). However, the accepted definitions are indeed
well-kinded and any rejected definitions would be accepted with a CUSK,
and so this wrinkle need not cause anyone to lose sleep.