[GHC] #15497: Coercion Quantification

[GHC]

#15497: Coercion Quantification
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D5054
       Wiki Page:                    |
  https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2|
-------------------------------------+-------------------------------------

Comment (by Richard Eisenberg <rae@…>):

 In [changeset:"ea5ade34788f29f5902c5475e94fbac13110eea5/ghc"
 ea5ade34/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="ea5ade34788f29f5902c5475e94fbac13110eea5"
 Coercion Quantification

 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
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler