[GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst) states that we allow `@k`-binders without standalone kind signatures: > Kind Inference > > When a declaration has no standalone kind signature, a `@k`-binder gives rise to a `forall k.` quantifier in the inferred kind signature. The inferred `forall k.` does not float to the left; the order of quantifiers continues to match the order of binders in the header. At the moment, however, we reject `@k`-binders in declarations without a signature: ```haskell -- No signature: type F @a (b :: a) = '(a, b) ``` Error message: ``` Test.hs:8:1: error: [GHC-92337] • Invalid invisible type variable binder: @a Either a standalone kind signature (SAKS) or a complete user-supplied kind (CUSK, legacy feature) is required to use invisible binders. • In the type synonym declaration for ‘F’ Suggested fix: Add a standalone kind signature for ‘F’ ``` Instead, GHC should have inferred `type F :: forall k. k -> (Type, k)`. The reason for this is an implementation difficulty described in `Note [No inference for invisible binders in type decls]`, cited here for completeness: ``` Note [No inference for invisible binders in type decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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. ``` It should be possible to implement this (I prefer the idea with a dedicated `->.` arrow), but it also doesn't seem worth the implementation cost until we find a compelling example.