[commit: ghc] master: Fix #15453: bug in ForAllCo case in opt_trans_rule (11de438)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/11de4380c2f16f374c6e8fbacf8dce00376e7efb/ghc

>---------------------------------------------------------------

commit 11de4380c2f16f374c6e8fbacf8dce00376e7efb
Author: Ningning Xie <xnningxie at gmail.com>
Date:   Sun Jul 29 13:15:33 2018 +0200

    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


>---------------------------------------------------------------

11de4380c2f16f374c6e8fbacf8dce00376e7efb
 compiler/types/OptCoercion.hs                      |  7 +++++-
 testsuite/tests/simplCore/should_compile/T15453.hs | 25 ++++++++++++++++++++++
 testsuite/tests/simplCore/should_compile/all.T     |  1 +
 3 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 70ae469..5dd7c0c 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -606,11 +606,16 @@ opt_trans_rule is co1 co2
 
   where
   push_trans tv1 eta1 r1 tv2 eta2 r2
+    -- Given:
+    --   co1 = \/ tv1 : eta1. r1
+    --   co2 = \/ tv2 : eta2. r2
+    -- Wanted:
+    --   \/tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])
     = 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
+      r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
 
 -- Push transitivity inside axioms
 opt_trans_rule is co1 co2
diff --git a/testsuite/tests/simplCore/should_compile/T15453.hs b/testsuite/tests/simplCore/should_compile/T15453.hs
new file mode 100644
index 0000000..a452bef
--- /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 58e9893..d4eaf19 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'])