diff options
| -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']) |