Changes between Version 92 and Version 93 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 14, 2008 7:13:48 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v92 v93  
    138138 * 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.) 
    139139 * For all local equalities, we `RECORD` substitutions for fresh flexibles introduced by `flatten` by already updating the meta type variable.  However, the update will only have an effect after the Insts have been zonked; i.e., after finalisation. 
     140 * We drop all loopy equalities (see Section 8.2 of our ICFP'08 paper).  If we drop a wanted, it is a type error; if we drop a local, we emit a warning (as we only sacrifice completeness). 
    140141 * We do the essentially same for class constraints; i.e., we use `flatten` to extract all family applications as equality constraints.  However, instead of adjusting the coercion at the flattened constraint, we generate a dictionary binding for the new dictionary (using a cast expression). 
    141142