Changes between Version 14 and Version 15 of TypeFunctionsSynTC
 Timestamp:
 Dec 12, 2006 8:33:32 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSynTC
v14 v15 479 479 === Normalisation of equalities === 480 480 481 Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` leads to a (possibly empty) set of normal equations, or to a type error. We proceed as follows:481 Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` (not containing schema variables) leads to a (possibly empty) set of normal equations, or to a type error. We proceed as follows: 482 482 483 483 1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`. … … 494 494 * Otherwise, fail. (Reason: a wobbly type variable, lack of left linearity, or nondecreasingness prevents us from obtaining a normal equation. If it is a wobbly type variable, the user can help by adding a type annotation; otherwise, we cannot handle the program without (maybe) losing decidability.) 495 495 496 Rejection of local assumptions that after normalisation are either not left linear or not decreasing may lead to incompleteness. However, this should only happen for programs that combine GADTs and type functions in ellaborate ways. (We still lack an example that produces such a situation, though.)496 Rejection of local assumptions that after normalisation are either not left linear or not decreasing may lead to incompleteness. However, this should only happen for programs that are invalid or combine GADTs and type functions in ellaborate ways. 497 497 498 498 '''TODO:''' I am wondering whether we can do that pulling out type family applications from lefthand sides and turning them into extra type equations lazily.