blob: 85e1b24dbedf553779675895a50b6a62373af5db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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 k (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')
|
