| | 116 | |
| | 117 | == Unification in the presence of type functions == |
| | 118 | |
| | 119 | We do ''not'' rewrite type function applications implicitly during unification. Instead, unifcation returns all ''required'' equalities that are non-syntactic. That has two advantages: (1) the computation of coercions is completely decoupled from unification and (2) unification does not have to know anything about equality axioms and given equalities. |
| | 120 | |
| | 121 | '''TODO:''' The whole extension would be a lot less invasive if we could arrange for unification to enter the required constraints into a pool in the monad instead of returning them (as the type of the unification routines would stay the same). Is this possible? |
| | 122 | |
| | 123 | Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates. |
| | 124 | |
| | 125 | |
