[Git][ghc/ghc][wip/backports] Fix handling of function coercions (#18747)
Ben Gamari
gitlab at gitlab.haskell.org
Mon Sep 28 21:00:13 UTC 2020
Ben Gamari pushed to branch wip/backports at Glasgow Haskell Compiler / GHC
Commits:
409f18b0 by Krzysztof Gogolewski at 2020-09-28T17:00:06-04:00
Fix handling of function coercions (#18747)
This was broken when we added multiplicity to the function type.
(cherry picked from commit e124f2a7d9a5932a4c2383fd3f9dd772b2059885)
- - - - -
4 changed files:
- compiler/GHC/Core/Coercion.hs
- + testsuite/tests/simplCore/should_compile/T18747A.hs
- + testsuite/tests/simplCore/should_compile/T18747B.hs
- testsuite/tests/simplCore/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1469,7 +1469,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
=====================================
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
=====================================
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
+
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -333,3 +333,6 @@ test('T18347', normal, compile, ['-dcore-lint -O'])
test('T18355', [ grep_errmsg(r'OneShot') ], compile, ['-O -ddump-simpl -dsuppress-uniques'])
test('T18399', normal, compile, ['-dcore-lint -O'])
test('T18589', normal, compile, ['-dcore-lint -O'])
+
+test('T18747A', normal, compile, [''])
+test('T18747B', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/409f18b00209b1d4c801fe4d282f1b302ded7105
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/409f18b00209b1d4c801fe4d282f1b302ded7105
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200928/48719ca0/attachment-0001.html>
More information about the ghc-commits
mailing list