Changes between Version 5 and Version 6 of Commentary/Compiler/Coercions


Ignore:
Timestamp:
Feb 14, 2011 1:26:16 PM (3 years ago)
Author:
megacz
Comment:

typo

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/Coercions

    v5 v6  
    1616 * Equality evidence variables ("type variables") are treated differently to dictionary evidence variables ("term varaibles"). This leads to lots of tiresome non-uniformities. 
    1717 * In an abstraction `/\a\x:a.e` the type variable `a` can appear in the type of a term-variable binder `x`.  In contrast `x` can't appear in the type of another binder.  Coercion binders behave exactly like term binders in this way, and quite unlike type binders. 
    18  * More seeriously, we don't have a decent way to handle superclass equalities. 
     18 * More seriously, we don't have a decent way to handle superclass equalities. 
    1919 
    2020The last problem is the one that triggered this note, and needs a bit more explanation.  Consider