30 | | 1. `co :: F t1..tn ~ t`, |

31 | | 2. `co :: x ~ t`, where `x` is a flexible type variable, or |

32 | | 3. `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable. |

| 30 | 1. '''Family equality:''' `co :: F t1..tn ~ t`, |

| 31 | 2. '''Flexible variable equality:''' `co :: x ~ t`, where `x` is a flexible type variable, or |

| 32 | 3. '''Rigid variable equality:''' `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable. |

36 | | * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, and |

37 | | * we call the Forms (2) & (3) '''variable equalities''', and require that the left- and right-hand side need to be different, and that the left-hand side does not occur in the right-hand side. |

| 36 | * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families and |

| 37 | * left-hand side of an equality may not occur in the right-hand side. |

| 38 | |

| 39 | The second bullet of the where clause is trivially true for equalities of Form (1) and it implies that the left- and right-hand sides are different. |