Arity inference in type declarations was introduced as a workaround for the lack of `@k`-binders. It's described in `Note [Arity inference in kcCheckDeclHeader_sig]`, cited here for completeness: ``` Note [Arity inference in kcCheckDeclHeader_sig] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider these declarations: type family S1 :: forall k2. k1 -> k2 -> Type type family S2 (a :: k1) (b :: k2) :: Type Both S1 and S2 can be given the same standalone kind signature: type S1 :: forall k1 k2. k1 -> k2 -> Type type S2 :: forall k1 k2. k1 -> k2 -> Type And, indeed, tyConKind S1 == tyConKind S2. However, tyConBinders and tyConResKind for S1 and S2 are different: tyConBinders S1 == [spec k1] tyConResKind S1 == forall k2. k1 -> k2 -> Type tyConKind S1 == forall k1 k2. k1 -> k2 -> Type tyConBinders S2 == [spec k1, spec k2, anon-vis (a :: k1), anon-vis (b :: k2)] tyConResKind S2 == Type tyConKind S1 == forall k1 k2. k1 -> k2 -> Type This difference determines the /arity/: tyConArity tc == length (tyConBinders tc) That is, the arity of S1 is 1, while the arity of S2 is 4. 'kcCheckDeclHeader_sig' needs to infer the desired arity, to split the standalone kind signature into binders and the result kind. It does so in two rounds: 1. matchUpSigWithDecl matches up - the [TyConBinder] from (applying splitTyConKind to) the kind signature - with the [LHsTyVarBndr] from the type declaration. That may leave some excess TyConBinder: in the case of S2 there are no excess TyConBinders, but in the case of S1 there are two (since there are no LHsTYVarBndrs. 2. Split off further TyConBinders (in the case of S1, one more) to make it possible to unify the residual return kind with the signature in the type declaration. More precisely, split off such enough invisible that the remainder of the standalone kind signature and the user-written result kind signature have the same number of invisible quantifiers. As another example consider the following declarations: type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type type family F a b type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type type family G a b :: forall r2. (r1, r2) -> Type For both F and G, the signature (after splitTyConKind) has sig_tcbs :: [TyConBinder] = [ anon-vis (@a_aBq), spec (@j_auA), anon-vis (@(b_aBr :: j_auA)) , spec (@k1_auB), spec (@k2_auC) , anon-vis (@(c_aBs :: (k1_auB, k2_auC)))] matchUpSigWithDecl will consume the first three of these, passing on excess_sig_tcbs = [ spec (@k1_auB), spec (@k2_auC) , anon-vis (@(c_aBs :: (k1_auB, k2_auC)))] For F, there is no result kind signature in the declaration for F, so we absorb all invisible binders into F's arity. The resulting arity of F is 3+2=5. Now, in the case of G, we have a result kind sig 'forall r2. (r2,r2)->Type'. This has one invisible binder, so we split of enough extra binders from our excess_sig_tcbs to leave just one to match 'r2'. res_ki = forall r2. (r1, r2) -> Type kisig = forall k1 k2. (k1, k2) -> Type ^^^ split off this one. The resulting arity of G is 3+1=4. ``` Now that we have `@k`-binders, we can significantly simplify all of this by simply removing arity inference altogether. As prescribed by [GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst), the arity of a type constructor shall be completely determined by SAKS zipping, without an additional arity inference step.