Changes between Version 100 and Version 101 of TypeFunctionsSolving
 Timestamp:
 Apr 14, 2009 7:48:12 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v100 v101 250 250 1. '''Substitution:''' 251 251 * '''Pass A:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''righthand side''' of all equalities. We also perform the same substitution on class constraints. 252 * '''Pass B:''' For any family equality of the form `co :: F t1..tn ~ alpha`, we apply the substitution `[F t1..tn/alpha]` to the '''both sides''' of all family equalities.252 * '''Pass B:''' Unless we are in inference mode, for any wanted family equality of the form `co :: F t1..tn ~ alpha`, we apply the substitution `[F t1..tn/alpha]` to '''both sides''' of all family equalities. We need to substitute all flexibles that arose as skolems during flattening of wanteds ''before'' we substitute any other flexibles. 253 253 2. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. Moreover, we have to do the same for equalities of the form `co :: F t1..tn ~ alpha` unless we are in inference mode and `alpha` appears in the environment or any other wanteds. (We never instantiate any flexibles introduced by flattening locals.) 254 The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. We need to instantiate all flexibles that arose as skolems during flattening of wanteds ''before'' we instantiate 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 nontermination of the combined classfamily solver. 254 255 Important points are the following: 256 * The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. 257 * 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 nontermination of the combined classfamily solver. 258 * We need to substitute family equalities into both sides of family equalities; consider, `F t1..tn ~ alpha, G s1..sm ~ alpha`. 255 259 256 260 Note that it is an important property of propagation that we only need to substitute into righthand sides during finalisation. After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above).