| 501 | |

| 502 | ---- |

| 503 | |

| 504 | == Maintaining type equations == |

| 505 | |

| 506 | The set of ''given'' equalities (i.e., those that we use as rewrite rules to normalise type terms) comprises two subsets: |

| 507 | |

| 508 | * ''Axioms'': The equations derived from type family instances. They are the only equations that may contain schema variables, and they are normal for well-formed programs. |

| 509 | * ''Local assumptions:'' The equations arising from equalities in signatures and from GADT pattern matching after normalisation. |

| 510 | |

| 511 | The set of axioms stays the same throughout type checking a module, whereas the set of local assumptions grows while descending into expressions and shrinks when ascending out of these expressions again. We have two different sorts of local assumptions: |

| 512 | |

| 513 | * ''Normal assumptions'': These are not altered anymore once they have been added to the set of local assumptions, until the moment when they are removed again. |

| 514 | * ''Semi-normal assumptions:'' These are only added tentatively. They are reconsidered whenever a new rule is added to the local assumptions, because a new rule may lead to further normalisation of semi-normal assumptions. If a semi-normal assumption is further normalised, the original assumption is removed and the further normalised one added (which can again trigger subsequent normalisation). NB: Strictly speaking, we can leave the original (semi-normal) equation in the set together with its further normalised version. |