Changes between Version 43 and Version 44 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 10, 2008 1:15:49 PM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v43 v44  
    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. 
    131131 * 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. 
    132  * We use !SubstFam and !SubstVar to substitute wanted equalities '''only''' if their right-hand side contains a flexible type variables (which for variable equalities means that we apply !SubstVar only to flexible variable equalities). 
     132 * We use !SubstFam and !SubstVar to substitute wanted equalities '''only''' if their right-hand side contains a flexible type variables (which for variable equalities means that we apply !SubstVar only to flexible variable equalities).  '''TODO:''' This is not sufficient while we are inferring a type signature as SPJ's example shows: `|- a ~ [x], a ~ [Int]`.  Here we want to infer `x := Int` before yielding `a ~ [Int]` as an irred.  So, we need to use !SubstVar and !SubstFam also if the rhs of a wanted contains a flexible variable.  This unfortunately makes termination more complicated. 
    133133 
    134134Notes: