blob: 00bade973aec384d0b0f513bed86936838dae34a (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T18747B where
import Data.Kind
import Data.Type.Equality
type family Sing :: k -> Type
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)
class SingKindX k => SingKind k where
toSing :: Demote k -> SomeSing k
type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a
type instance Demote Bool = Bool
type instance Promote Bool = Bool
data Foo (a :: Type) where MkFoo :: Foo Bool
data SFoo :: forall a. Foo a -> Type where
SMkFoo :: SFoo MkFoo
type instance Sing = SFoo
type instance Demote (Foo a) = Foo (DemoteX a)
type instance Promote (Foo a) = Foo (PromoteX a)
instance SingKindX a => SingKind (Foo a) where
toSing MkFoo = SomeSing SMkFoo
|
