[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 generalizing the reflexive coercion to
> {{{#!hs
>   | GRefl Role Type MCoercion
> }}}
> As its name suggests, and as its typing rule makes precise, `GRefl` is
> generalised version of `Refl`:
>
> {{{
>      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 form will replace both `Refl` and the current
> `CoherenceCo`:
>
> {{{#!hs
>   | Refl Role Type
>
>   -- Coherence applies a coercion to the left-hand type of another
> coercion
>   -- See Note [Coherence]
>   | CoherenceCo Coercion KindCoercion
>      -- :: e -> N -> e
> }}}
>
> When the `MCoercion` is `MRefl`, `GRefl` is just the same as `Refl`.
>
> It is easy to express `CoherenceCo` using `GRefl`.  If `g1 :: s ~r t`,
> then
> {{{
> CoherenceCo g1 g2        :: (s |> g2) ~r t
> Sym (GRefl r s g2) ; g1  :: (s |> g1) ~r t
> }}}

New description:

 This patch aims at generalizing the reflexive coercion to
 {{{#!hs
   | GRefl Role Type MCoercion
 }}}
 As its name suggests, and as its typing rule makes precise, `GRefl` is
 generalised version of `Refl`:

 {{{
      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 any
 coercion (MCo co). To know more about MCoercion see
 [https://ghc.haskell.org/trac/ghc/ticket/14975 #14975].

 This new coercion form will replace both `Refl` and the current
 `CoherenceCo`:

 {{{#!hs
   | Refl Role Type

   -- Coherence applies a coercion to the left-hand type of another
 coercion
   -- See Note [Coherence]
   | CoherenceCo Coercion KindCoercion
      -- :: e -> N -> e
 }}}

 When the `MCoercion` is `MRefl`, `GRefl` is just the same as `Refl`.

 It is easy to express `CoherenceCo` using `GRefl`.  If `g1 :: s ~r t`,
 then
 {{{
 CoherenceCo g1 g2        :: (s |> g2) ~r t
 Sym (GRefl r s g2) ; g1  :: (s |> g1) ~r t
 }}}

--

Comment (by ningning):

 We don't know coercion {{{co}}} in {{{MCo co}}} is reflexive or not.

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