|
|
Summary:
Given
```
co1 = \/ tv1 : eta1. r1
co2 = \/ tv2 : eta2. r2
```
We would like to optimize `co1; co2` so we push transitivity inside forall.
It should be
```
\/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
```
It is implemented in the ForAllCo case in opt_trans_rule in OptCoercion.
However current implementation is not right:
```
r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded!
```
This patch corrects it to be
```
r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
```
Test Plan: validate
Reviewers: bgamari, goldfire, RyanGlScott
Reviewed By: RyanGlScott
Subscribers: rwbarton, thomie, carter
GHC Trac Issues: #15453
Differential Revision: https://phabricator.haskell.org/D5018
|
