[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:                    |
-------------------------------------+-------------------------------------

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