[commit: ghc] master: Fix #15725 with an extra Sym (48efbc0)
git at git.haskell.org
git at git.haskell.org
Mon Oct 15 09:43:13 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/48efbc04bd45d806c52376641e1a7ed7278d1ec7/ghc
>---------------------------------------------------------------
commit 48efbc04bd45d806c52376641e1a7ed7278d1ec7
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date: Mon Oct 15 10:25:02 2018 +0200
Fix #15725 with an extra Sym
Summary:
We were adding a `Sym` to one argument in the `InstCo`
case of `optCoercion` but not another, leading to the two arguments
to misaligned when combined via `Trans`. This fixes the issue with
a well targeted use of `wrapSym`.
Test Plan: make test TEST=T15725
Reviewers: goldfire, ningning, bgamari
Reviewed By: goldfire, ningning
Subscribers: rwbarton, carter
GHC Trac Issues: #15725
Differential Revision: https://phabricator.haskell.org/D5217
>---------------------------------------------------------------
48efbc04bd45d806c52376641e1a7ed7278d1ec7
compiler/types/OptCoercion.hs | 33 ++++++----
testsuite/tests/dependent/should_compile/T15725.hs | 74 ++++++++++++++++++++++
testsuite/tests/dependent/should_compile/all.T | 1 +
3 files changed, 97 insertions(+), 11 deletions(-)
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 8a44b86..1d48ed0 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -377,9 +377,9 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
| Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
- (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
- -- kind_co :: k1 ~ k2
- -- arg' :: (t1 :: k1) ~ (t2 :: k2)
+ (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
+ -- mkSymCo kind_co :: k1 ~ k2
+ -- sym_arg :: (t1 :: k1) ~ (t2 :: k2)
-- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
sym rep r co_body
@@ -396,23 +396,34 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
| Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
= opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
- (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
+ (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
False False r' co_body'
-- forall over coercion...
| Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
- , CoercionTy h1 <- t1
- , CoercionTy h2 <- t2
- = let new_co = mk_new_co cv' kind_co' h1 h2
+ , CoercionTy h1' <- t1'
+ , CoercionTy h2' <- t2'
+ = let new_co = mk_new_co cv' kind_co' h1' h2'
in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
False False r' co_body'
| otherwise = InstCo co1' arg'
where
- co1' = opt_co4_wrap env sym rep r co1
- r' = chooseRole rep r
- arg' = opt_co4_wrap env sym False Nominal arg
- Pair t1 t2 = coercionKind arg'
+ co1' = opt_co4_wrap env sym rep r co1
+ r' = chooseRole rep r
+ arg' = opt_co4_wrap env sym False Nominal arg
+ sym_arg = wrapSym sym arg'
+
+ -- Performance note: don't be alarmed by the two calls to coercionKind
+ -- here, as only one call to coercionKind is actually demanded per guard.
+ -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used
+ -- when checking if co1' (i.e., co1 post-optimization) is a forall.
+ --
+ -- t1/t2 must come from sym_arg, not arg', since it's possible that arg'
+ -- might have an extra Sym at the front (after being optimized) that co1
+ -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725)
+ Pair t1 t2 = coercionKind sym_arg
+ Pair t1' t2' = coercionKind arg'
mk_new_co cv kind_co h1 h2
= let -- h1 :: (t1 ~ t2)
diff --git a/testsuite/tests/dependent/should_compile/T15725.hs b/testsuite/tests/dependent/should_compile/T15725.hs
new file mode 100644
index 0000000..a5f259e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15725.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15725 where
+
+import Data.Functor.Identity (Identity(..))
+import Data.Kind (Type)
+import GHC.Exts (Any)
+
+-----
+-- The important bits
+-----
+
+type instance Meth (x :: Identity a) = GenericMeth x
+instance SC Identity
+
+-------------------------------------------------------------------------------
+
+data family Sing :: forall k. k -> Type
+data instance Sing :: forall a. Identity a -> Type where
+ SIdentity :: Sing x -> Sing ('Identity x)
+
+newtype Par1 p = Par1 p
+data instance Sing :: forall p. Par1 p -> Type where
+ SPar1 :: Sing x -> Sing ('Par1 x)
+
+type family Rep1 (f :: Type -> Type) :: Type -> Type
+
+class PGeneric1 (f :: Type -> Type) where
+ type From1 (z :: f a) :: Rep1 f a
+ type To1 (z :: Rep1 f a) :: f a
+
+class SGeneric1 (f :: Type -> Type) where
+ sFrom1 :: forall (a :: Type) (z :: f a). Sing z -> Sing (From1 z)
+ sTo1 :: forall (a :: Type) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
+
+type instance Rep1 Identity = Par1
+
+instance PGeneric1 Identity where
+ type From1 ('Identity x) = 'Par1 x
+ type To1 ('Par1 x) = 'Identity x
+
+instance SGeneric1 Identity where
+ sFrom1 (SIdentity x) = SPar1 x
+ sTo1 (SPar1 x) = SIdentity x
+
+type family GenericMeth (x :: f a) :: f a where
+ GenericMeth x = To1 (Meth (From1 x))
+
+type family Meth (x :: f a) :: f a
+
+class SC f where
+ sMeth :: forall a (x :: f a).
+ Sing x -> Sing (Meth x)
+ default sMeth :: forall a (x :: f a).
+ ( SGeneric1 f, SC (Rep1 f)
+ , Meth x ~ GenericMeth x
+ )
+ => Sing x -> Sing (Meth x)
+ sMeth sx = sTo1 (sMeth (sFrom1 sx))
+
+ dummy :: f a -> ()
+ dummy _ = ()
+
+type instance Meth (x :: Par1 p) = x
+instance SC Par1 where
+ sMeth x = x
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5f6e901..1bf6cc7 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -55,3 +55,4 @@ test('T15346', normal, compile, [''])
test('T15419', normal, compile, [''])
test('T14066h', normal, compile, [''])
test('T15666', normal, compile, [''])
+test('T15725', normal, compile, [''])
More information about the ghc-commits
mailing list