testsuite: Add test for #15346

Test case: dependent/should_compile/T{15346,15419}.

3 files changed, 88 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_compile/T15346.hs b/testsuite/tests/dependent/should_compile/T15346.hs
new file mode 100644
index 0000000000..3d8d49b9d2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15346.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeApplications #-}
+module T15346 where
+
+import Data.Kind
+import Data.Proxy
+
+-----
+
+type family Rep (a :: Type) :: Type
+type instance Rep () = ()
+
+type family PFrom (x :: a) :: Rep a
+
+-----
+
+class SDecide k where
+  test :: forall (a :: k). Proxy a
+
+instance SDecide () where
+  test = undefined
+
+test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
+test1 = seq (test @_ @(PFrom a)) Proxy
+
+test2 :: forall (a :: ()). Proxy a
+test2 = test1
diff --git a/testsuite/tests/dependent/should_compile/T15419.hs b/testsuite/tests/dependent/should_compile/T15419.hs
new file mode 100644
index 0000000000..68f20e5604
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15419.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15419 where
+
+import Data.Kind
+
+data Prod a b
+data Proxy p = Proxy
+
+-----
+
+data family Sing :: forall k. k -> Type
+data instance Sing x = STuple
+
+-----
+
+type family Rep1 (f :: k -> Type) :: k -> Type
+type instance Rep1 ((,) a) = Prod a
+
+type family From1 (f :: Type -> Type) a (z :: f a) :: Rep1 f a
+type family To1 (f :: Type -> Type) a (z :: Rep1 f a) :: f a
+
+class Generic1 (f :: Type -> Type) where
+  sFrom1 :: forall (a :: Type) (z :: f a).      Proxy z -> Sing (From1 f a z)
+  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Proxy r -> Proxy (To1 f a r :: f a)
+
+instance Generic1 ((,) a) where
+  sFrom1 Proxy = undefined
+  sTo1   Proxy = undefined
+
+-----
+
+type family Fmap (g :: b) (x :: f a) :: f b
+type instance Fmap (g :: b) (x :: (u, a)) = To1 ((,) u) b (Fmap g (From1 ((,) u) a x))
+
+class PFunctor (f :: Type -> Type) where
+  sFmap         :: forall a b (g :: b) (x :: f a).
+                   Proxy g -> Sing x -> Proxy (Fmap g x)
+
+instance PFunctor (Prod a) where
+  sFmap _ STuple = undefined
+
+sFmap1 :: forall (f :: Type -> Type) (u :: Type) (b :: Type) (g :: b) (x :: f u).
+                 (Generic1 f,
+                  PFunctor (Rep1 f),
+                  Fmap g x ~ To1 f b (Fmap g (From1 f u x)) )
+              => Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap1 sg sx = sTo1 (sFmap sg (sFrom1 sx))
+
+sFmap2  :: forall (p :: Type) (a :: Type) (b :: Type) (g :: b) (x :: (p, a)).
+          Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap2 = sFmap1
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 64782c0276..4e096c1f71 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -51,3 +51,5 @@ test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
 test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
+test('T15346', normal, compile, [''])
+test('T15419', normal, compile, [''])