Test Trac #9144

3 files changed, 42 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T9144.hs b/testsuite/tests/polykinds/T9144.hs
new file mode 100644
index 0000000000..0a9ef08afa
--- /dev/null
+++ b/testsuite/tests/polykinds/T9144.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, RankNTypes #-}
+
+module T9144 where
+
+import Data.Proxy
+import GHC.TypeLits
+
+data family Sing (a :: k)
+
+data SomeSing :: KProxy k -> * where
+  SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
+
+class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
+  fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
+  toSing :: DemoteRep ('KProxy :: KProxy k) -> SomeSing ('KProxy :: KProxy k)
+
+type family DemoteRep (kproxy :: KProxy k) :: *
+
+data Foo = Bar Nat
+data FooTerm = BarTerm Integer
+
+data instance Sing (x :: Foo) where
+  SBar :: Sing n -> Sing (Bar n)
+
+type instance DemoteRep ('KProxy :: KProxy Nat) = Integer
+type instance DemoteRep ('KProxy :: KProxy Foo) = FooTerm
+
+instance SingKind ('KProxy :: KProxy Nat) where
+  fromSing = undefined
+  toSing = undefined
+
+instance SingKind ('KProxy :: KProxy Foo) where
+  fromSing (SBar n) = BarTerm (fromSing n)
+  toSing n = case toSing n of SomeSing n' -> SomeSing (SBar n')
diff --git a/testsuite/tests/polykinds/T9144.stderr b/testsuite/tests/polykinds/T9144.stderr
new file mode 100644
index 0000000000..f2c65530ee
--- /dev/null
+++ b/testsuite/tests/polykinds/T9144.stderr
@@ -0,0 +1,7 @@
+

+T9144.hs:34:26:

+    Couldn't match type ‘Integer’ with ‘FooTerm’

+    Expected type: DemoteRep 'KProxy

+      Actual type: DemoteRep 'KProxy

+    In the first argument of ‘toSing’, namely ‘n’

+    In the expression: toSing n

diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 96faa6725b..09c72545a0 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -101,3 +101,4 @@ test('T7481', normal, compile_fail,[''])
 test('T8705', normal, compile, [''])
 test('T8985', normal, compile, [''])
 test('T9106', normal, compile_fail, [''])
+test('T9144', normal, compile_fail, [''])