Changes between Version 44 and Version 45 of TypeFunctionsSolving
 Timestamp:
 Aug 10, 2008 1:40:05 PM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v44 v45 130 130 * 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 nontermination. 131 131 * We should probably use !SubstVar on all variable equalities before using !SubstFam, as the former may refine the lefthand 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 righthand 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. 132 * We use !SubstFam and !SubstVar to substitute wanted equalities '''only''' if their righthand 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. However, SPJ also observed that we really only need to substitute variables in lefthand sides (not in righthand sides) as far as enabling other rewrites goes. However, there are trick problems left as the following two examples show ` a~c, a~b, c~a` and ` b ~ c, b ~ a, a ~ b, c ~ a`. 133 133 134 134 Notes: