diff options
| author | Ningning Xie <xnningxie@gmail.com> | 2018-07-29 13:15:33 +0200 |
|---|---|---|
| committer | Krzysztof Gogolewski <krz.gogolewski@gmail.com> | 2018-07-29 13:15:34 +0200 |
| commit | 11de4380c2f16f374c6e8fbacf8dce00376e7efb (patch) | |
| tree | 00f5e3fbc6834419005124ac11fbc2afcd5257d5 | |
| parent | 3539561b24b78aee2b37280ddf6bb64e2db3a67d (diff) | |
| download | haskell-11de4380c2f16f374c6e8fbacf8dce00376e7efb.tar.gz | |
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
| -rw-r--r-- | compiler/types/OptCoercion.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/simplCore/should_compile/T15453.hs | 25 | ||||
| -rw-r--r-- | testsuite/tests/simplCore/should_compile/all.T | 1 |
3 files changed, 32 insertions, 1 deletions
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 70ae469795..5dd7c0c935 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 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 58e98937ec..d4eaf196df 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']) |