| 121 | | '''TODO:''' Partition the rules depending on which if the three forms of normal equalities they apply to!!! |
| | 121 | '''TODO:''' |
| | 122 | * Rules applying to family equalities: |
| | 123 | * IdenticalLHS only applies to family equalities (both local and wanteds) |
| | 124 | * Top only applies to family equalities (both locals and wanteds) |
| | 125 | We should apply IdenticalLHS first as it cheaper and potentially reduces the number of applications of Top. |
| | 126 | * Rules applying to variable equalities: |
| | 127 | * Unify only applies to all wanted flexible variable equalities |
| | 128 | * Subst (= local for variable equalities) applies to all variable equalities, where local variable equalities are substituted into all equalities, but wanted variable equalities are only substituted into wanted equalities. |
| | 129 | We should first apply Unify where possible and, only when that is exhausted, apply Subst. This is as Unify is cheaper and has global impact (instantiates variables in the environment, too). |
