Changes between Version 1 and Version 2 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 22, 2008 7:03:18 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v1 v2  
    66== Normal equalities == 
    77 
    8 Central to the algorithm are '''normal equalities''', which can be regarded as a set of rewrite rules.  Normal equalities are carefully oriented and contain applications of synonym family applications only in outermost positions of left-hand sides.  They assume one of the following three forms: 
     8Central to the algorithm are '''normal equalities''', which can be regarded as a set of rewrite rules.  Normal equalities are carefully oriented and contain synonym families only as the head symbols of left-hand sides.  They assume one of the following three forms: 
    99 
    1010 1. `co :: F t1..tn ~ t`, 
     
    1212 3. `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable. 
    1313 
    14 and `t`, `t1`, ..., `tn` contain no applications of synonym families.  Coercions `co` are either wanteds (represented by a flexible type variable) or givens (represented by type term of kind CO). 
     14The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families.  Moreover, in Forms (2) & (3), the left- and right-hand side need to be different, and the left-hand side may not occur in the right-hand side. 
    1515 
    16 NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 
     16Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO). 
     17 
     18Important to note is the following: 
     19 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 
     20 * Rewrite rules of the forms described under Cases (2) & (3) require extra care during rewriting.  They may only be applied if they are ''not'' recursive. 
     21 
     22In GHC, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules. 
     23 
     24 
     25== Termination == 
     26 
     27The Note [skolemOccurs loop] in the old code explains that equalities of the form `x ~ t` (where `x` is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify.  As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule !SkolemOccurs as rewrite rules.  For this to work, !SkolemOccurs also had to apply to equalities of the form `a ~ t[[a]]`.  This was a somewhat intricate set up that's being simplified in the new algorithm.  Whether equalities of the form `x ~ t` are used as rewrite rules or solved by Unify doesn't matter anymore.  Instead, we are careful to not use equalities of Form (2) or (3) for rewriting if their left-hand side symbol occurs in the right-hand side.