Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information