Skip to content

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 and GHC.Core.Coercion.liftCoSubstCoVarBndrUsing,
  • go_forall in GHC.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).

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