Note [No inference for invisible binders in type decls]

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

Suppose we have (#22560):
   data T @k (a::k) = MkT (...(T ty)...)
What monokind can we give to T after step 1 of the kind inference
algorithm described in Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]?
Remember: Step 1 generates a MonoTcTyCon.

It can't be
  T :: kappa1 -> kappa2 -> Type
because the invocation `(T ty)` doesn't have a visible argument for `kappa`.
Nor can it be
  T :: forall k. kappa2 -> Type
because that breaks the Monomorphic Recursion Principle: MonoTcTyCons have
monomorphic kinds; see Note [No polymorphic recursion in type decls]. It could be
  T :: kappa1 ->. kappa2 -> type
where `->.` is a new kind of arrow in kinds, which (like a type-class argument
in terms) is invisibly instantiated.  Or we could fake it with
  T :: forall _. kappa2 -> Type
where `_` is a completely fresh variable, but that seems very smelly and makes it
harder to talk about the Monomorphic Recursion Principle.  Moreover we'd need
some extra fancy types in TyConBinders to record this extra information.

Note that in *terms* we do not allow
  f @a (x::a) = rhs
unless `f` has a type signature.  So we do the same for types:

  We allow `@` binders in data type declarations ONLY if the
  type constructor has a standalone kind signature (or a CUSK).

That means that GHC.Tc.Gen.HsType.kcInferDeclHeader, which is used when we
don't have a kind signature or CUSK, and builds a MonoTcTyCon, we can simply
reject invisible binders outright (GHC.Tc.Gen.HsType.rejectInvisibleBinders);
and continue to use mkAnonTyConBinders as described in
Note [No polymorphic recursion in type decls].

If we get cries of pain we can revist this decision.