Changes between Version 37 and Version 38 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 7, 2008 7:15:20 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v37 v38  
    129129  * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds) 
    130130 * With !SubstFam and !SubstVar, we always substitute locals into wanteds and never the other way around.  We perform substitutions exhaustively.  For !SubstVar, this is crucial to avoid non-termination. 
     131 * We should probably use !SubstVar on all variable equalities before using !SubstFam, as the former may refine the left-hand sides of family equalities, and hence, lead to Top being applicable where it wasn't before. 
    131132 
    132133Notes: 
    133134 
    134  * In principle, a variable equality could be discarded after an exhaustive application of !SubstVar.  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.  That reasoning definitely applies to local equalities, but I think it also applies to wanteds (and I think that GHC so far never applies wanteds to class dictionaries, which might explain some of the failing tests.) 
     135 * In principle, a variable equality could be discarded after an exhaustive application of !SubstVar.  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.  That reasoning definitely applies to local equalities, but I think it also applies to wanteds (and I think that GHC so far never applies wanteds to class dictionaries, which might explain some of the failing tests.)  Flexible variable equalities cannot be discarded in any case as we need them for finalisation. 
    135136 
    136137=== Observations === 
     
    148149 * (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.) 
    149150* '''TODO:''' Now that we delay instantiation until after solving, do we still need to prioritise flexible variables equalities over rigid ones?  (Probably not.) 
     151 
     152 
     153== Examples == 
     154 
     155=== !SubstFun on two wanteds is crucial === 
     156 
     157{{{ 
     158Top: F Int ~ [Int] 
     159 
     160  |- F delta ~ [delta], F delta ~ [Int] 
     161(SubstFam) 
     162  |- F delta ~ [delta], norm [[ [delta] ~ [Int] ]] 
     163== 
     164  |- F delta ~ [delta], delta ~ Int 
     165(SubstVar) 
     166  |- norm [[ F Int ~ [Int] ]], delta ~ Int 
     167== 
     168  |- F Int ~ [Int], delta ~ Int 
     169(Top) 
     170  |- norm [[ [Int] ~ [Int] ]], delta ~ Int 
     171== 
     172  |- delta ~ Int 
     173QED 
     174}}} 
    150175 
    151176