[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 ningning):

 Replying to [comment:4 simonpj]:
 > Can you elaborate?
 >
 > * What are the advantages of the new form?  (It looks more symmetrical;
 but it has more arguments.)   Can you say what the "several places" where
 is is useful are?  Are there any disadvanatages?

 - Theoretically, this new form emphasizes that type equality relation is
 coherent, namely coercions within types is immaterial. This is studied in
 Section 5.8.3 in
 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs/
 Richard's thesis] and the {{{An-EraseEq}}} rule in
 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs/
 A Specification for Dependent Types in Haskell paper]
 - Practically, it simplifies some sort of coercion constructions. In
 current implementation, coercions as {{{t |> g ~ t}}} is built as {{{ <t>
 |> g}}}. Namely we build the reflexivity coercion first and insert kind
 coercion to the left. Using the new form it can be rewritten to {{{ (t |>
 g)  ~ t }}}. Similarly, coercions as {{{ t ~ t |> g }}} is {{{sym (<t> |>
 g)}}}, and can be rewritten to {{{ t ~ (t |> g) }}} directly. We have
 several usage like that in current implementation, e.g. {{{TcCanonical}}}.
 Moreover, one possible optimization is to replace the {{{buildCoercion ::
 Type -> Type -> CoercionN}}} function in module {{{Coercion}}}, which
 builds a coercion between types that are the same ignoring coercions,
 which is exactly the intention of the new form.
 - There are indeed some disadvantages now. In current refactor, there are
 three places where given a coercion {{{g}}}, we need to call
 {{{coercionKind}}} to get {{{g :: t1 ~ t2}}} in order to use the new form
 because the new form needs this information to build {{{(t1 |> ki_co) ~ t1
 ; g }}}. This is very inefficient. We are still trying to figure out
 further optimizations in those places.


 > * Can we use the new form in `OptCoercion` to simplify coercions?

 We have optimizations for {{{EraseEqCo}}} in {{{OptCoercion}}}. For
 example {{{opt_co4}}} and {{{opt_trans_rule}}} for the new form are both
 simpler than for the old form. Besides that, I don't know if further
 optimization is possible?


 > * I see no constraints on `r` in the rule. So you could fix on `N` and
 use `SubCo` to downgrade to `R`?

 It is doable I think. But I don't know if we could gain any benefit from
 this restriction?

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