summaryrefslogtreecommitdiff
path: root/testsuite/tests/polykinds/T9144.hs
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')