Note [No polymorphic recursion in type decls]

GHC/Tc/TyCl.hs:875 compiler 1 ticket

In GHC.Tc.HsType.kcInferDeclHeader we use mkAnonTyConBinders to make
the TyConBinders for the MonoTcTyCon.  Here is why.

Should this kind-check (cf #16344)?
  data T ka (a::ka) b  = MkT (T Type           Int   Bool)
                             (T (Type -> Type) Maybe Bool)

Notice that T is used at two different kinds in its RHS.  No!
This should not kind-check.  Polymorphic recursion is known to
be a tough nut.

Many moons ago, we laboriously (with help from the renamer) tried to give T
the polymorphic kind
   T :: forall ka -> ka -> kappa -> Type
where kappa is a unification variable, even in the inferInitialKinds phase
(which is what kcInferDeclHeader is all about).  But that is dangerously
fragile (see #16344), because `kappa` might get unified with `ka`, and
depending on just /when/ that unification happens, the instantiation of T's
kind would vary between different call sites of T.

We encountered similar trickiness with invisible binders in type
declarations: see Note [No inference for invisible binders in type decls]

Solution: the Monomorphic Recursion Principle:

    A MonoTcTyCon has a monomoprhic kind (no foralls!)

See the invariants on MonoTcTyCon in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon].

So kcInferDeclHeader gives T a straightforward monomorphic kind, with no
quantification whatsoever. That's why we always use mkAnonTyConBinder for
all arguments when figuring out tc_binders.

But notice that (#16344 comment:3)

* Consider this declaration:
    data T2 ka (a::ka) = MkT2 (T2 Type a)

  Starting with inferInitialKinds
  (Step 1 of Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]):
    MonoTcTyCon binders:
      ka[tyv] :: (kappa1[tau] :: Type)
       a[tyv] :: (ka[tyv]     :: Type)
    MonoTcTyCon kind:
      T2 :: kappa1[tau] -> ka[tyv] -> Type

  Given this kind for T2, in Step 2 we kind-check (T2 Type a)
  from where we see
    T2's first arg:  (kappa1 ~ Type)
    T2's second arg: (ka ~ ka)
  These constraints are soluble by (kappa1 := Type)
  so generaliseTcTyCon (Step 3) gives
    T2 :: forall (k::Type) -> k -> *

  But now the /typechecking/ (Step 4, aka desugaring, tcTyClDecl)
  phase fails, because the call (T2 Type a) in the RHS is ill-kinded.

  We'd really prefer all errors to show up in the kind checking phase.

* This algorithm still accepts (in all phases)
     data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
  although T3 is really polymorphic-recursive too.
  Perhaps we should somehow reject that.