Apply a substitution to the type variable binders of an associated type family. This is used to compute default instances for associated type families (see tcATDefault) as well as newtype-derived associated type family instances (see gen_Newtype_fam_insts in GHC.Tc.Deriv.Generate).

As a concrete example, consider the following class and associated type family:

  class C k (a :: k) where
    type F k a (b :: k) :: Type
    type F j p q = (Proxy j p, Proxy j (q :: j))

If a user defines this instance:

instance C (Type -> Type) Maybe where {}

Then in order to typecheck the default F instance, we must apply the substitution [k :-> (Type -> Type), a :-> Maybe] to F's binders, which are [k, a, (b :: k)]. The result should look like this:

  type F (Type -> Type) Maybe (b :: Type -> Type) =
    (Proxy (Type -> Type) Maybe, Proxy (Type -> Type) (b :: Type -> Type))

Making this work requires some care. There are two cases:

If we encounter a type variable in the domain of the substitution (e.g., k or a), then we apply the substitution directly.
Otherwise, we substitute into the type variable's kind (e.g., turn b :: k to b :: Type -> Type). We then return an extended substitution where the old b (of kind k) maps to the new b (of kind Type -> Type).

This step is important to do in case there are later occurrences of b, which we must ensure have the correct kind. Otherwise, we might end up with Proxy @(Type -> Type) (b :: k) on the right-hand side of the default instance, which would be completely wrong.

Contrast substATBndrs function with similar substitution functions:

substTyVars does not substitute into the kinds of each type variable, nor does it extend the substitution. substTyVars is meant for occurrences of type variables, whereas substATBndrs is meant for binders.
substTyVarBndrs does substitute into kinds and extends the substitution, but it does not apply the substitution to the variables themselves. As such, substTyVarBndrs returns a list of TyVars rather than a list of Types.