Note [Bad TyCon telescopes]

Now that we can mix type and kind variables, there are an awful lot of
ways to shoot yourself in the foot. Here are some.

  data SameKind :: k -> k -> *   -- just to force unification

1.  data T1 a k (b :: k) (x :: SameKind a b)

The problem here is that we discover that a and b should have the same
kind. But this kind mentions k, which is bound *after* a.
(Testcase: dependent/should_fail/BadTelescope)

2.  data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

Note that b is not bound. Yet its kind mentions a. Because we have
a nice rule that all implicitly bound variables come before others,
this is bogus.

To catch these errors, we call checkTyConTelescope during kind-checking
datatype declarations.  This checks for

* Ill-scoped binders. From (1) and (2) above we can get putative
  kinds like
       T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> *
  where 'k' is mentioned a's kind before k is bound

  This is easy to check for: just look for
  out-of-scope variables in the kind

* We should arguably also check for ambiguous binders
  but we don't.  See Note [Ambiguous kind vars].

See also
  * Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl.
  * Note [Checking telescopes] in GHC.Tc.Types.Constraint discusses how
    this check works for `forall x y z.` written in a type.