1 | | = Normalising and Solving Type Equalities = |

| 1 | = Entailment of Type Equalities = |

| 2 | |

| 3 | Our aims is to derive the entailment judgement |

| 4 | {{{ |

| 5 | g1, .., gn |- w1, .., wm |

| 6 | }}} |

| 7 | i.e., whether we can derive the wanted equalities `w1` to `wm` from the given equalities `g1`, .., `gn` under a given set of toplevel equality schemas (i.e., equalities involving universally quantified variables). We permit unification variables in the wanted equalities, and a derivation may include the instantiation of these variables; i.e., may compute a unifier. However, that unifer must be most general. |

| 8 | |

| 9 | The derivation algorithm is complicated by the pragmatic requirement that, even if there is no derivation for the judgement, we would like to compute a unifier. This unifier should be as specific as possible under some not yet specified (strongest) weakening of the judgement so that it is derivable. (Whatever that means...) |