Changes between Version 3 and Version 4 of TypeFunctions/IntegratedSolver

Dec 3, 2008 11:47:52 AM (6 years ago)



  • TypeFunctions/IntegratedSolver

    v3 v4  
    7070Currently, `tcImproveOne` generates pairs of types to be unified (on the basis of the FD improvement rules) and does unify them with `unifyType` (via `unifyEqns`).  In the integrated solver, `tcImproveOne` should generate equality constraints (with identity coercions) instead.  This will get rid of the `extra_eqs` that we currently have in `reduceContext`. 
     74=== Additional points raised during phone conf, 3 Dec === 
     76The plan is to outline on this page, the final design we are aiming for (independent of whether we implement it in one rewrite of the source or more). 
     78==== Orientation of normal variable equalities ==== 
     80Currently, when we finalise `alpha ~> beta`, we may decide to instantiate `beta` with `alpha` (in `uMeta`).  We should not make the choice about which way to instantiate at that late stage.  Instead, we should adjust the < relation between type variables to orient them already such that the instantiation is always in the direction of the rewrite rule.  That just seems cleaner. 
     82==== Treatment of variable instantiation ==== 
     84Instead of instantiating type variables during finalisation, we should already remove equalities of the form `co :w alpha ~> t` during normalisation or propagation and remember them as substitutions `alpha := t` in `EqConfig` (or similar) and instantiate `co := id`.  We also need to ensure that the substitution is propagated to all other constraints. 
     86When we return to `reduceContext` and solve the implication constraint, we also got to use the substitutions as given equalities when we try to solve the implications. 
     88==== !EqConfig ==== 
     90`EqConfig` needs to become more general and be a general solver configuration.  Likewise `RewriteInst` needs to include a variant for class constraints, which we need to handle during propagate.