Changes between Version 26 and Version 27 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 9:26:33 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v26 v27  
    116116== Solving == 
    117117 
     118Notes: 
     119 
    118120 * (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 - just as in new-single.) 
    119121 
     
    122124 In principle, a rewrite rule could be discarded after an exhaustive application of (Local).  However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around. 
    123125 
    124  * (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local).  '''SLPJ''' good point: in view of (Local) there's no need for (IdenticalLHS) to deal with a given `a~t`.  So if epsilon1 is 'g', the LHS could be restricted to form `F t1..tn` which would be good (in the paper).[[BR]][[BR]] 
    125  '''SLPJ''' but why do you say that we don't want IdenticalLHS on wanteds?  What about `F a ~ x1, F a ~ Int`.  Then we could unify the HM variable `x` with `Int`. 
     126 * (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local).   BUT as SLPJ points out what about `F a ~ x1, F a ~ Int`?  Then we could unify the HM variable `x` with `Int`. 
    126127 
    127128=== Observations ===