[GHC] #15192: Refactor of Coercion

[GHC]

#15192: Refactor of Coercion
-------------------------------------+-------------------------------------
        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:D4747
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by sweirich):

 This new form may be more efficient if there are multiple uses of
 Coherence needed --- one EraseEqCo can stand in for many casts (on either
 side).

 However, If coherence has better sharing in some situations, then perhaps
 we don't want to lose that information.

 There is no reason why we can't have both in the implementation.   At
 least until we can see if EraseEqCo is useful in connection with other
 extensions.  Richard and I both found it useful in generating coercions in
 our proofs. Perhaps that will show up in some of the coercions that GHC
 needs to construct.

 Eventually, we may want to get rid of both of these coercions. In other
 words --- we can allow Core to work "up-to-erasure-equivalence", as in the
 system in the appendix of Richard's thesis.  In that case, we wouldn't
 need to use Coherence or EraseEqCo very much (If at all).

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