#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