Commit e124f2a7 authored by Krzysztof Gogolewski's avatar Krzysztof Gogolewski Committed by Marge Bot
Browse files

Fix handling of function coercions (#18747)

This was broken when we added multiplicity to the function type.
parent 160fba4a
......@@ -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
......
{-# 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
{-# 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
......@@ -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, [''])
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