29 | | * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. |

30 | | * (Local) only applies to normalised equalities in Form (2) & (3). After an application of (Local), the rewrite rule can be discarded |

| 30 | * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. Moreover, it only applies to wanted equalities. (Rationale: Local equality constraints don't justify global instantiation of flexible type variables.) |

| 31 | * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds. After an '''exhaustive''' application of (Local), the rewrite rule can be discarded |

| 32 | |