Changes between Version 62 and Version 63 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 20, 2008 9:09:05 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v62 v63  
    130130 * 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 right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.) 
    131131 * We flatten locals and wanteds in the same manner, using fresh flexible type variables.  (We have flexibles in locals anyway and don't use (Unify) during normalisation - this is different to `new-single`.) 
     132 
     133 
     134'''TODO:''' We may want to drop the `alpha > x for all x already used` side condition on fresh `alpha`s again.  Instead, we should probably consider all ''local'' flexible variable equalities during finalisation, too.  At least, those involving flexible variables introduced by flattening. 
    132135 
    133136