Fix handling of function coercions (#18747)wip/T18747

This was broken when we added multiplicity to the function type.

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, [''])