Changes between Version 2 and Version 3 of TypeFunctionsSynTC/GHC


Ignore:
Timestamp:
Jan 17, 2007 1:35:53 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/GHC

    v2 v3  
    2020 * ''Left linear'': No schema variable appears more than once in `s`. 
    2121 * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family occuring in `t` must be strictly less than the number of data type constructor and variable symbols in `s`. 
     22 * ''Rank 0'': No foralls in `s` or `t`. 
    2223 
    2324Examples of normal type equations: 
     
    4950=== Normalisation of equalities === 
    5051 
    51 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: 
     52Normalisation of an equality `s = t` of arbitrary rank-0 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: 
    5253 
    5354 1. Reduce `s` and `t` to NF, giving us `s'` and `t'`.