Changes between Version 2 and Version 3 of TypeFunctionsSolving
 Timestamp:
 Jul 22, 2008 7:14:46 AM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v2 v3 16 16 Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO). 17 17 18 Important to note is the following: 19 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 20 * Rewrite rules of the forms described under Cases (2) & (3) require extra care during rewriting. They may only be applied if they are ''not'' recursive. 18 NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 21 19 22 20 In GHC, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules. 23 21 24 22 23 == Normalisation == 24 25 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check. (Immediate rejection is always justified, as righthand sides do not contain synonym familles; hence, any recursive occurrences of a lefthand side imply that the equality is unsatisfiable.) 26 25 27 == Termination == 26 28 27 The Note [skolemOccurs loop] in the old code explains that equalities of the form `x ~ t` (where `x` is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify. As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule !SkolemOccurs as rewrite rules. For this to work, !SkolemOccurs also had to apply to equalities of the form `a ~ t[[a]]`. This was a somewhat intricate set up that's being simplified in the new algorithm. Whether equalities of the form `x ~ t` are used as rewrite rules or solved by Unify doesn't matter anymore. Instead, we are careful to not use equalities of Form (2) or (3) for rewriting if their lefthand side symbol occurs in the righthand side.29 The Note [skolemOccurs loop] in the old code explains that equalities of the form `x ~ t` (where `x` is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify. As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule !SkolemOccurs as rewrite rules. For this to work, !SkolemOccurs also had to apply to equalities of the form `a ~ t[[a]]`. This was a somewhat intricate set up that's being simplified in the new algorithm. Whether equalities of the form `x ~ t` are used as rewrite rules or solved by Unify doesn't matter anymore. Instead, we disallow recursive equalities completely. This is possible as righthand sides are free of synonym families.