#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