• 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.
    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
TcErrors.hs 127 KB