Remove arity inference in type declarations
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", the arity of a type constructor shall be completely determined by SAKS zipping, without an additional arity inference step.