Changes between Version 31 and Version 32 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 4, 2008 12:11:59 PM (7 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v31 v32  
    4545 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.
    4646 * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same.
    47  * Normal equalities are '''never''' recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities.
     47 * Normal equalities are '''never''' self-recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities.  '''SLPJ''' why.  What prevents `a ~ [b], b ~ [a]`? 
    4848
    4949=== Coercions ===
     
    5757Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules.
    5858
     59'''SLPJ''': I propose that we use a proper data type, not `Either` for this.
    5960
    6061== Normalisation ==