• simonpj@microsoft.com's avatar
    Tidy up coercions, and implement csel1, csel2, cselR · bcadca67
    simonpj@microsoft.com authored
    In preparation for implementing the PushC rule for coercion-swizzling
    in the Simplifier, I had to inmplement the three new decomposition
    operators for coercions, which I've called csel1, csel2, and cselR.
    
         co :: ((s1~t1) => r1) ~ ((s2~t2) => r2)
         ---------------------------------------
                  csel1 co :: s1~s2
    
    and similarly csel2, cselR.
    
    On the way I fixed the coercionKind function for types of form
              (s1~t2) => r2
    which currently are expressed as a forall type.  
    
    And I refactored quite a bit to help myself understand what is
    going on.
    bcadca67
Coercion.lhs 32.6 KB