Use Name instead of TyVar in ForAllCo
Currently, the ForAllCo
constructor of Coercion
stores a TyVar
:
data Coercion
= ...
| ForAllCo TyCoVar KindCoercion Coercion
This means on top of storing the Name
we are also storing a Kind
. However, we can recover the kind as the LHS kind of the kind coercion, so we don't need to store it separately. The suggestion in this ticket is to replace TyCoVar
with Name
in the ForAllCo
constructor. Note that the typing rule for ForAllCo
does not change: when we have ForAllCo name kco co
, then occurrences of name
in co
must have kind k1
, where kco :: k1 ~# k2
.
One reason to make this change is that storing the LHS kind separately means we often have to update it (using setVarType
). Example calls of setVarType
:
-
GHC.Core.Coercion.liftCoSubstTyVarBndrUsing
andGHC.Core.Coercion.liftCoSubstCoVarBndrUsing
, -
go_forall
inGHC.Core.Coercion.coercionRKind
, -
GHC.Core.Type.occCheckExpand
.
This can cause problems with directed coercions, as we might not have enough information to hand to be able to compute the updated kind. So one goal of this ticket is to allow us to change the substitution lifting mechanism to work with directed coercions instead of coercions (which isn't possible with the call to coercionLKind
in GHC.Core.Coercion.lift{Ty,Co}SubstTyVarBndrUsing
, which is only needed because we are storing the kind separately in ForAllCo
).