Changes between Version 105 and Version 106 of TypeFunctionsSolving
- Apr 21, 2009 3:48:53 AM (8 years ago)
v105 v106 261 261 Important points are the following: 262 262 * The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. 263 263 264 * We need to substitute all flexibles that arose as skolems during flattening of wanteds ''before'' we substitute any other flexibles. Consider `F delta ~ alpha, F alpha ~ delta`, where `alpha` is a skolem and `delta` a free flexible. We need to produce `F (F delta) ~ delta` (and not `F (F alpha) ~ alpha`). Otherwise, we may wrongly claim to having performed an improvement, which can lead to non-termination of the combined class-family solver. 264 265 * We need to substitute family equalities into both sides of family equalities; consider, `F t1..tn ~ alpha, G s1..sm ~ alpha`.