#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