#15192: Refactor of Coercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15192 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler