Changes between Version 20 and Version 21 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 3:18:23 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v20 v21  
    3737Conor's alternative general idea: 
    3838 * (B) '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' 
    39 This is a bit more permissive than (A).  For example 
     39Remember "unification succeeds" means "overlap detected", so (B) is a bit more permissive than (A).  For example 
    4040{{{ 
    41   type instance F x   x    = blah 
    42   type instance F Int Bool = boo 
     41  type instance Good x   x    = blah 
     42  type instance Good Int Bool = boo 
    4343}}} 
    4444These would be considered overlapping by (A), but accepted as non-overlapping (ie unification fails) by (B).  And indeed these two are fine (ie cannot give rise to unsoundness).