GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-09-06T08:26:38Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15192Refactor of Coercion2021-09-06T08:26:38ZNingning XieRefactor of CoercionThis 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
--------------...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 [\#14975](https://ghc.haskell.org/trac/ghc/ticket/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
```8.6.1Ningning XieNingning Xie