Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T9144.hs
1 {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, RankNTypes #-}
2
3 module T9144 where
4
5 import Data.Proxy
6 import GHC.TypeLits
7
8 data family Sing (a :: k)
9
10 data SomeSing :: KProxy k -> * where
11 SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
12
13 class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
14 fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
15 toSing :: DemoteRep ('KProxy :: KProxy k) -> SomeSing ('KProxy :: KProxy k)
16
17 type family DemoteRep (kproxy :: KProxy k) :: *
18
19 data Foo = Bar Nat
20 data FooTerm = BarTerm Integer
21
22 data instance Sing (x :: Foo) where
23 SBar :: Sing n -> Sing (Bar n)
24
25 type instance DemoteRep ('KProxy :: KProxy Nat) = Integer
26 type instance DemoteRep ('KProxy :: KProxy Foo) = FooTerm
27
28 instance SingKind ('KProxy :: KProxy Nat) where
29 fromSing = undefined
30 toSing = undefined
31
32 instance SingKind ('KProxy :: KProxy Foo) where
33 fromSing (SBar n) = BarTerm (fromSing n)
34 toSing n = case toSing n of SomeSing n' -> SomeSing (SBar n')