• Ningning Xie's avatar
    Coercion Quantification · ea5ade34
    Ningning Xie authored
    This patch corresponds to #15497.
    
    According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
     we would like to have coercion quantifications back. This will
    allow us to migrate (~#) to be homogeneous, instead of its current
    heterogeneous definition. This patch is (lots of) plumbing only. There
    should be no user-visible effects.
    
    An overview of changes:
    
    - Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
    but only in *Core*. All relevant functions are updated accordingly.
    - Small changes that should be irrelevant to the main task:
        1. removed dead code `mkTransAppCo` in Coercion
        2. removed out-dated Note Computing a coercion kind and
           roles in Coercion
        3. Added `Eq4` in Note Respecting definitional equality in
           TyCoRep, and updated `mkCastTy` accordingly.
        4. Various updates and corrections of notes and typos.
    - Haddock submodule needs to be changed too.
    
    Acknowledgments:
    This work was completed mostly during Ningning Xie's Google Summer
    of Code, sponsored by Google. It was advised by Richard Eisenberg,
    supported by NSF grant 1704041.
    
    Test Plan: ./validate
    
    Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar
    
    Subscribers: RyanGlScott, monoidal, rwbarton, carter
    
    GHC Trac Issues: #15497
    
    Differential Revision: https://phabricator.haskell.org/D5054
    ea5ade34
TcErrors.hs 127 KB