Test Trac #9144
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 27 May 2014 21:27:44 +0000 (22:27 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 27 May 2014 22:15:51 +0000 (23:15 +0100)
testsuite/tests/polykinds/T9144.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9144.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

diff --git a/testsuite/tests/polykinds/T9144.hs b/testsuite/tests/polykinds/T9144.hs
new file mode 100644 (file)
index 0000000..0a9ef08
--- /dev/null
@@ -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 (file)
index 0000000..f2c6553
--- /dev/null
@@ -0,0 +1,7 @@
+\r
+T9144.hs:34:26:\r
+    Couldn't match type ‘Integer’ with ‘FooTerm’\r
+    Expected type: DemoteRep 'KProxy\r
+      Actual type: DemoteRep 'KProxy\r
+    In the first argument of ‘toSing’, namely ‘n’\r
+    In the expression: toSing n\r
index 96faa67..09c7254 100644 (file)
@@ -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, [''])