Changes between Version 7 and Version 8 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 4:25:40 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v7 v8  
    2323 * Perform Rule Triv as part of normalisation.
    2424 * 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.)
     25 * Use flexible tyvars for flattening of locals, too.
    2526
    2627
    2728== Solving ==
    2829
    29  * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families.
    30  * (Local) only applies to normalised equalities in Form (2) & (3).  After an application of (Local), the rewrite rule can be discarded
     30 * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families.  Moreover, it only applies to wanted equalities.  (Rationale: Local equality constraints don't justify global instantiation of flexible type variables.)
     31 * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds.  After an '''exhaustive''' application of (Local), the rewrite rule can be discarded
     32
    3133
    3234== Termination ==