Changes between Version 102 and Version 103 of TypeFunctionsSolving


Ignore:
Timestamp:
Apr 21, 2009 1:31:46 AM (5 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v102 v103  
    261261 * 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. 
    262262 * We need to substitute family equalities into both sides of family equalities; consider, `F t1..tn ~ alpha, G s1..sm ~ alpha`. 
    263  
    264 Note that it is an important property of propagation that we only need to substitute into right-hand sides during finalisation.  After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above). 
     263 * We must not substitute family equalities into right-hand sides of variable equalities.  (If the variable equality directly or indirectly instantiates a flexible that is free in the environment, we would instantiate it with a family application, which we set out to avoid.) 
     264 * There is no need to substitute family equalities into dictionaries as they cannot influence instance selection. 
     265 
     266Note that it is an important property of propagation that we need to substitute variable equalities only into right-hand sides during finalisation.  After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above). 
    265267 
    266268== Examples ==