Commit eb2b71c5 authored by Ningning Xie's avatar Ningning Xie Committed by Ben Gamari

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 11de4380)
parent 79e13610
......@@ -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
......
{-# 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
......@@ -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'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment