Changes between Version 11 and Version 12 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 1:57:40 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v11 v12  
    3636 
    3737This new overlap check only looks at the ''left hand side'' of the instance. The alert reader will know that GHC currently also looks at the ''right hand side'', which we return to in "coincident overlap" below. 
     38 
     39== Coincident overlap ==  
     40 
     41In the official release of GHC, it is permitted to write something like this: 
     42 
     43{{{ 
     44type instance F Int = Int 
     45type instance F a   = a 
     46}}} 
     47 
     48These instances surely overlap, but in the case when they do, the right-hand sides coincide. We call this '''coincident overlap'''. 
     49 
     50However, the above proposal of linearising the LHS before checking overlap makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. So the proposal abandons support for coincident overlap between standalone type instances.  However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
     51 
    3852 
    3953== Branched instances ==