Changes between Version 7 and Version 8 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 4:25:40 AM (6 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 ==