Changes between Version 15 and Version 16 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 12, 2006 8:34:02 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v15 v16  
    481481Normalisation 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: 
    482482 
    483  1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`. 
     483 1. Reduce `s` and `t` to NF, giving us `s'` and `t'`. 
    484484 2. If `s'` and `t'` are the same variable, we succeed (with no new rule). 
    485485 3. If `s'` or `t'` is a rigid variable, we fail.  (Reason: cannot instantiate rigid variables.)