Changes between Version 43 and Version 44 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Dec 28, 2006 8:17:47 PM (9 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v43 v44  
    114114'''TODO:''' Where do we perform the detailed check of well-formedness of equalities?  In `check_pred_ty` or when adding given equalities? 
    115115 
     116 
     117== Unification in the presence of type functions == 
     118 
     119We do ''not'' rewrite type function applications implicitly during unification.  Instead, unifcation returns all ''required'' equalities that are non-syntactic.  That has two advantages: (1) the computation of coercions is completely decoupled from unification and (2) unification does not have to know anything about equality axioms and given equalities. 
     120 
     121'''TODO:''' The whole extension would be a lot less invasive if we could arrange for unification to enter the required constraints into a pool in the monad instead of returning them (as the type of the unification routines would stay the same).  Is this possible? 
     122 
     123Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates. 
     124 
     125 
    116126== Type checking expressions == 
    117127