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 Xiehttps://gitlab.haskell.org/ghc/ghc/-/issues/15453Bug in opt_trans_rule in OptCoercion2019-07-07T18:04:49ZNingning XieBug in opt_trans_rule in OptCoercionThe ForAllCo case in the definition of opt_trans_rule in OptCoercion is not right:
```hs
push_trans tv1 eta1 r1 tv2 eta2 r2
= fireTransRule "EtaAllTy" co1 co2 $
mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
...The ForAllCo case in the definition of opt_trans_rule in OptCoercion is not right:
```hs
push_trans tv1 eta1 r1 tv2 eta2 r2
= fireTransRule "EtaAllTy" co1 co2 $
mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` tv1
r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded!
```
Given `co1;co2`, where
```hs
co1 = \/ tv1 : eta1. r1
co2 = \/ tv2 : eta2. r2
```
We would like optimize the transitivity coercion. I think what we want is
```hs
\/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
```
Namely it should be
```hs
r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
```
If there is any program that could hit the bug it would be better, as we can add it to test cases.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Bug in opt_trans_rule in OptCoercion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The ForAllCo case in the definition of opt_trans_rule in OptCoercion is not right:\r\n\r\n{{{#!hs\r\n push_trans tv1 eta1 r1 tv2 eta2 r2\r\n = fireTransRule \"EtaAllTy\" co1 co2 $\r\n mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')\r\n where\r\n is' = is `extendInScopeSet` tv1\r\n r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded!\r\n}}}\r\n\r\nGiven {{{co1;co2}}}, where\r\n\r\n{{{#!hs\r\n co1 = \\/ tv1 : eta1. r1\r\n co2 = \\/ tv2 : eta2. r2\r\n}}}\r\n\r\nWe would like optimize the transitivity coercion. I think what we want is\r\n\r\n{{{#!hs\r\n\\/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])\r\n}}}\r\n\r\nNamely it should be\r\n\r\n{{{#!hs\r\nr2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2\r\n}}}\r\n\r\nIf there is any program that could hit the bug it would be better, as we can add it to test cases.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Ningning XieNingning Xie