28 | | Central to the algorithm are '''normal equalities''', which can be regarded as a set of rewrite rules. Normal equalities are carefully oriented and contain synonym families only as the head symbols of left-hand sides. They assume one of the following three forms: |

29 | | |

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. |

| 28 | Central to the algorithm are '''normal equalities''', which can be regarded as a set of rewrite rules. Normal equalities are carefully oriented and contain synonym families only as the head symbols of left-hand sides. They assume one of the following two major forms: |

| 29 | |

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

| 31 | 2. '''Variable equality:''' `co :: a ~ t`, where we again distinguish two forms: |

| 32 | a. '''Variable-term equality.''' `co :: a ~ t`, where `t` is '''not''' a variable, or |

| 33 | b. '''Variable-variable equality.''' `co :: a ~ b`, where `a < b`. |

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. |

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

| 38 | * the left-hand side of an equality may not occur in the right-hand side, and |

| 39 | * the relation `a < b` is a total order on type variables, where `x < a` whenever `x` is a flexible and `a` a rigid type variable (otherwise, the details of the total order are irrelevant). |