Fix #15453: bug in ForAllCo case in opt_trans_rule

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

(cherry picked from commit 11de4380c2f16f374c6e8fbacf8dce00376e7efb)

2 files changed, 26 insertions, 0 deletions

diff --git a/testsuite/tests/simplCore/should_compile/T15453.hs b/testsuite/tests/simplCore/should_compile/T15453.hs
new file mode 100644
index 0000000000..a452bef0df
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T15453.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15453 where
+
+import Data.Kind
+import Data.Proxy
+import Data.Type.Equality
+
+type family S :: Type where
+  S = T
+type family T :: Type where
+  T = Int
+
+f :: (forall (x :: S). Proxy x) :~: (forall (x :: T). Proxy x)
+f = Refl
+
+g :: (forall (x :: T). Proxy x) :~: (forall (x :: Int). Proxy x)
+g = Refl
+
+h :: (forall (x :: S). Proxy x) :~: (forall (x :: Int). Proxy x)
+h = f `trans` g
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 5ad7dba94a..fe9cb05ec0 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -316,3 +316,4 @@ test('T15005', normal, compile, ['-O'])
 # we omit profiling because it affects the optimiser and makes the test fail
 test('T15056', [extra_files(['T15056a.hs']), omit_ways(['profasm'])], multimod_compile, ['T15056', '-O -v0 -ddump-rule-firings'])
 test('T15186', normal, multimod_compile, ['T15186', '-v0'])
+test('T15453', normal, compile, ['-dcore-lint -O1'])