Fix #15453: bug in ForAllCo case in opt_trans_rule
authorNingning Xie <xnningxie@gmail.com>
Sun, 29 Jul 2018 11:15:33 +0000 (13:15 +0200)
committerBen Gamari <ben@smart-cactus.org>
Wed, 1 Aug 2018 00:24:39 +0000 (20:24 -0400)
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)

compiler/types/OptCoercion.hs
testsuite/tests/simplCore/should_compile/T15453.hs [new file with mode: 0644]
testsuite/tests/simplCore/should_compile/all.T

index db4bc8c..213c0a7 100644 (file)
@@ -594,11 +594,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 (file)
index 0000000..a452bef
--- /dev/null
@@ -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
index 5ad7dba..fe9cb05 100644 (file)
@@ -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'])