diff options
author | Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io> | 2020-09-26 01:02:28 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-09-26 13:19:36 -0400 |
commit | e124f2a7d9a5932a4c2383fd3f9dd772b2059885 (patch) | |
tree | 87e1161f0c0c7b9d076d67c638e19be7c3a40909 | |
parent | 160fba4aa306c0649c72a6dcd7c98d9782a0e74b (diff) | |
download | haskell-e124f2a7d9a5932a4c2383fd3f9dd772b2059885.tar.gz |
Fix handling of function coercions (#18747)
This was broken when we added multiplicity to the function type.
-rw-r--r-- | compiler/GHC/Core/Coercion.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/simplCore/should_compile/T18747A.hs | 82 | ||||
-rw-r--r-- | testsuite/tests/simplCore/should_compile/T18747B.hs | 50 | ||||
-rw-r--r-- | testsuite/tests/simplCore/should_compile/all.T | 2 |
4 files changed, 135 insertions, 1 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 47e6d40173..6ba6c0f144 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -1486,7 +1486,7 @@ instCoercion (Pair lty rty) g w | isFunTy lty && isFunTy rty -- g :: (t1 -> t2) ~ (t3 -> t4) -- returns t2 ~ t4 - = Just $ mkNthCo Nominal 3 g -- extract result type, which is the 4th argument to (->) + = Just $ mkNthCo Nominal 4 g -- extract result type, which is the 5th argument to (->) | otherwise -- one forall, one funty... = Nothing diff --git a/testsuite/tests/simplCore/should_compile/T18747A.hs b/testsuite/tests/simplCore/should_compile/T18747A.hs new file mode 100644 index 0000000000..4904234524 --- /dev/null +++ b/testsuite/tests/simplCore/should_compile/T18747A.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module T18747A where + +import Data.Kind +import Data.Type.Equality + +type family Sing :: k -> Type +data SomeSing :: Type -> Type where + SomeSing :: Sing (a :: k) -> SomeSing k + +data SList :: forall a. [a] -> Type where + SNil :: SList '[] + SCons :: Sing x -> Sing xs -> SList (x:xs) +type instance Sing = SList + +data Univ = U1 | K1 Type | Sum Univ Univ | Product Univ Univ + +data SUniv :: Univ -> Type where + SU1 :: SUniv U1 + SK1 :: Sing c -> SUniv (K1 c) + SSum :: Sing a -> Sing b -> SUniv (Sum a b) + SProduct :: Sing a -> Sing b -> SUniv (Product a b) +type instance Sing = SUniv + +data In :: Univ -> Type where + MkU1 :: In U1 + MkK1 :: c -> In (K1 c) + L1 :: In a -> In (Sum a b) + R1 :: In b -> In (Sum a b) + MkProduct :: In a -> In b -> In (Product a b) + +data SIn :: forall u. In u -> Type where + SMkU1 :: SIn MkU1 + SMkK1 :: Sing c -> SIn (MkK1 c) + SL1 :: Sing a -> SIn (L1 a) + SR1 :: Sing b -> SIn (R1 b) + SMkProduct :: Sing a -> Sing b -> SIn (MkProduct a b) +type instance Sing = SIn + +class Generic (a :: Type) where + type Rep a :: Univ + from :: a -> In (Rep a) + to :: In (Rep a) -> a + +class PGeneric (a :: Type) where + type PFrom (x :: a) :: In (Rep a) + type PTo (x :: In (Rep a)) :: a + +class SGeneric k where + sFrom :: forall (a :: k). Sing a -> Sing (PFrom a) + sTo :: forall (a :: In (Rep k)). Sing a -> Sing (PTo a :: k) + sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a + sFot :: forall (a :: In (Rep k)). Sing a -> PFrom (PTo a :: k) :~: a + +instance Generic [a] where + type Rep [a] = Sum U1 (Product (K1 a) (K1 [a])) + from [] = L1 MkU1 + from (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs)) + to (L1 MkU1) = [] + to (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs + +instance PGeneric [a] where + type PFrom '[] = L1 MkU1 + type PFrom (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs)) + type PTo (L1 MkU1) = '[] + type PTo (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs + +instance SGeneric [a] where + sFrom SNil = SL1 SMkU1 + sFrom (SCons x xs) = SR1 (SMkProduct (SMkK1 x) (SMkK1 xs)) + sTo (SL1 SMkU1) = SNil + sTo (SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))) = SCons x xs + sTof SNil = Refl + sTof SCons{} = Refl + sFot (SL1 SMkU1) = Refl + sFot (SR1 (SMkProduct SMkK1{} SMkK1{})) = Refl diff --git a/testsuite/tests/simplCore/should_compile/T18747B.hs b/testsuite/tests/simplCore/should_compile/T18747B.hs new file mode 100644 index 0000000000..00bade973a --- /dev/null +++ b/testsuite/tests/simplCore/should_compile/T18747B.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module T18747B where + +import Data.Kind +import Data.Type.Equality + +type family Sing :: k -> Type + +data SomeSing (k :: Type) where + SomeSing :: Sing (a :: k) -> SomeSing k + +type family Promote (k :: Type) :: Type +type family PromoteX (a :: k) :: Promote k + +type family Demote (k :: Type) :: Type +type family DemoteX (a :: k) :: Demote k + +type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a) + +class SingKindX k => SingKind k where + toSing :: Demote k -> SomeSing k + +type instance Demote Type = Type +type instance Promote Type = Type +type instance DemoteX (a :: Type) = Demote a +type instance PromoteX (a :: Type) = Promote a + +type instance Demote Bool = Bool +type instance Promote Bool = Bool + +data Foo (a :: Type) where MkFoo :: Foo Bool + +data SFoo :: forall a. Foo a -> Type where + SMkFoo :: SFoo MkFoo +type instance Sing = SFoo + +type instance Demote (Foo a) = Foo (DemoteX a) +type instance Promote (Foo a) = Foo (PromoteX a) + +instance SingKindX a => SingKind (Foo a) where + toSing MkFoo = SomeSing SMkFoo + diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T index 1535e32253..d9541e9318 100644 --- a/testsuite/tests/simplCore/should_compile/all.T +++ b/testsuite/tests/simplCore/should_compile/all.T @@ -338,3 +338,5 @@ test('T18603', normal, compile, ['-dcore-lint -O']) # T18649 should /not/ generate a specialisation rule test('T18649', normal, compile, ['-O -ddump-rules -Wno-simplifiable-class-constraints']) +test('T18747A', normal, compile, ['']) +test('T18747B', normal, compile, ['']) |