#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: | -------------------------------------+------------------------------------- Old description:
This patch aims at defining the new coercion rule
{{{#!hs | EraseEqCo Role Type Type KindCoercion -- "e" -> _ -> _ -> N -> e }}}
which corresponds to the typing rule
{{{ t1 : k1 t2 : k2 |t1| = |t2| g : k1 ~ k2 ------------------------------------ EraseEqCo r t1 t2 g : t1 ~r t2 }}}
Namely, if two types after erasure of casts and coercions are equivalent, then they can be casted from and to each other. This new coercion rule is designed to replace the current coherence rule
{{{#!hs -- Coherence applies a coercion to the left-hand type of another coercion -- See Note [Coherence] | CoherenceCo Coercion KindCoercion -- :: e -> N -> e }}}
The new rule is useful in several places. For example, now it is easier to define coercion {{{t |> k ~ t}}} without resorting to reflexivity coercion, and {{{t ~ t |> k}}} without resorting to symmetric rule.
New description: This patch aims at generalizing the reflexive coercion to {{{#!hs | GRefl Role Type MCoercion }}} which corresponds to the typing rule {{{ t1 : k1 ------------------------------------ GRefl r t1 MRefl: t1 ~r t1 t1 : k1 co :: k1 ~ k2 ------------------------------------ GRefl r t1 (MCo co) : t1 ~r t1 |> co }}} {{{MCoercion}}} wraps a coercion, which might be reflexive (MRefl) or not (MCo co). To know more about MCoercion see [https://ghc.haskell.org/trac/ghc/ticket/14975 #14975]. This new coercion rule will replace the current coherence rule {{{#!hs -- Coherence applies a coercion to the left-hand type of another coercion -- See Note [Coherence] | CoherenceCo Coercion KindCoercion -- :: e -> N -> e }}} -- Comment (by ningning): Update the ticket from {{{EraseEqCo}}} to {{{GRefl}}} according to the discussion with Richard and Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15192#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler