singletons-2.7: tests/compile-and-dump/Singletons/T159.golden
Singletons/T159.hs:0:0:: Splicing declarations
genSingletons [''T0, ''T1]
======>
type ASym0 = 'A :: T0
type BSym0 = 'B :: T0
type CSym0 = 'C :: T0
type DSym0 = 'D :: T0
type ESym0 = 'E :: T0
type FSym0 = 'F :: T0
type ST0 :: T0 -> GHC.Types.Type
data ST0 z
where
SA :: ST0 ('A :: T0)
SB :: ST0 ('B :: T0)
SC :: ST0 ('C :: T0)
SD :: ST0 ('D :: T0)
SE :: ST0 ('E :: T0)
SF :: ST0 ('F :: T0)
type instance Sing @T0 = ST0
instance SingKind T0 where
type Demote T0 = T0
fromSing SA = A
fromSing SB = B
fromSing SC = C
fromSing SD = D
fromSing SE = E
fromSing SF = F
toSing A = SomeSing SA
toSing B = SomeSing SB
toSing C = SomeSing SC
toSing D = SomeSing SD
toSing E = SomeSing SE
toSing F = SomeSing SF
instance SingI 'A where
sing = SA
instance SingI 'B where
sing = SB
instance SingI 'C where
sing = SC
instance SingI 'D where
sing = SD
instance SingI 'E where
sing = SE
instance SingI 'F where
sing = SF
type N1Sym0 = 'N1 :: T1
type C1Sym0 :: (~>) T0 ((~>) T1 T1)
data C1Sym0 a0123456789876543210
where
C1Sym0KindInference :: SameKind (Apply C1Sym0 arg) (C1Sym1 arg) =>
C1Sym0 a0123456789876543210
type instance Apply C1Sym0 a0123456789876543210 = C1Sym1 a0123456789876543210
instance SuppressUnusedWarnings C1Sym0 where
suppressUnusedWarnings = snd (((,) C1Sym0KindInference) ())
infixr 5 `C1Sym0`
type C1Sym1 :: T0 -> (~>) T1 T1
data C1Sym1 a0123456789876543210 a0123456789876543210
where
C1Sym1KindInference :: SameKind (Apply (C1Sym1 a0123456789876543210) arg) (C1Sym2 a0123456789876543210 arg) =>
C1Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (C1Sym1 a0123456789876543210) a0123456789876543210 = C1Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (C1Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) C1Sym1KindInference) ())
infixr 5 `C1Sym1`
type C1Sym2 (a0123456789876543210 :: T0) (a0123456789876543210 :: T1) =
'C1 a0123456789876543210 a0123456789876543210 :: T1
infixr 5 `C1Sym2`
type (:&&@#@$) :: (~>) T0 ((~>) T1 T1)
data (:&&@#@$) a0123456789876543210
where
(::&&@#@$###) :: SameKind (Apply (:&&@#@$) arg) ((:&&@#@$$) arg) =>
(:&&@#@$) a0123456789876543210
type instance Apply (:&&@#@$) a0123456789876543210 = (:&&@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:&&@#@$) where
suppressUnusedWarnings = snd (((,) (::&&@#@$###)) ())
infixr 5 :&&@#@$
type (:&&@#@$$) :: T0 -> (~>) T1 T1
data (:&&@#@$$) a0123456789876543210 a0123456789876543210
where
(::&&@#@$$###) :: SameKind (Apply ((:&&@#@$$) a0123456789876543210) arg) ((:&&@#@$$$) a0123456789876543210 arg) =>
(:&&@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:&&@#@$$) a0123456789876543210) a0123456789876543210 = (:&&@#@$$$) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:&&@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::&&@#@$$###)) ())
infixr 5 :&&@#@$$
type (:&&@#@$$$) (a0123456789876543210 :: T0) (a0123456789876543210 :: T1) =
'(:&&) a0123456789876543210 a0123456789876543210 :: T1
infixr 5 :&&@#@$$$
type ST1 :: T1 -> GHC.Types.Type
data ST1 z
where
SN1 :: ST1 ('N1 :: T1)
SC1 :: forall (n :: T0) (n :: T1).
(Sing n) -> (Sing n) -> ST1 ('C1 n n :: T1)
(:%&&) :: forall (n :: T0) (n :: T1).
(Sing n) -> (Sing n) -> ST1 ('(:&&) n n :: T1)
type instance Sing @T1 = ST1
instance SingKind T1 where
type Demote T1 = T1
fromSing SN1 = N1
fromSing (SC1 b b) = (C1 (fromSing b)) (fromSing b)
fromSing ((:%&&) b b) = ((:&&) (fromSing b)) (fromSing b)
toSing N1 = SomeSing SN1
toSing (C1 (b :: Demote T0) (b :: Demote T1))
= case
((,) (toSing b :: SomeSing T0)) (toSing b :: SomeSing T1)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing ((SC1 c) c) }
toSing ((:&&) (b :: Demote T0) (b :: Demote T1))
= case
((,) (toSing b :: SomeSing T0)) (toSing b :: SomeSing T1)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:%&&) c) c) }
infixr 5 `SC1`
infixr 5 :%&&
instance SingI 'N1 where
sing = SN1
instance (SingI n, SingI n) =>
SingI ('C1 (n :: T0) (n :: T1)) where
sing = (SC1 sing) sing
instance SingI (C1Sym0 :: (~>) T0 ((~>) T1 T1)) where
sing = (singFun2 @C1Sym0) SC1
instance SingI d => SingI (C1Sym1 (d :: T0) :: (~>) T1 T1) where
sing = (singFun1 @(C1Sym1 (d :: T0))) (SC1 (sing @d))
instance (SingI n, SingI n) =>
SingI ('(:&&) (n :: T0) (n :: T1)) where
sing = ((:%&&) sing) sing
instance SingI ((:&&@#@$) :: (~>) T0 ((~>) T1 T1)) where
sing = (singFun2 @(:&&@#@$)) (:%&&)
instance SingI d =>
SingI ((:&&@#@$$) (d :: T0) :: (~>) T1 T1) where
sing = (singFun1 @((:&&@#@$$) (d :: T0))) ((:%&&) (sing @d))
Singletons/T159.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| infixr 5 :||
infixr 5 `C2`
data T2 = N2 | C2 T0 T2 | T0 :|| T2 |]
======>
data T2 = N2 | C2 T0 T2 | T0 :|| T2
infixr 5 `C2`
infixr 5 :||
type N2Sym0 = N2 :: T2
type C2Sym0 :: (~>) T0 ((~>) T2 T2)
data C2Sym0 a0123456789876543210
where
C2Sym0KindInference :: SameKind (Apply C2Sym0 arg) (C2Sym1 arg) =>
C2Sym0 a0123456789876543210
type instance Apply C2Sym0 a0123456789876543210 = C2Sym1 a0123456789876543210
instance SuppressUnusedWarnings C2Sym0 where
suppressUnusedWarnings = snd (((,) C2Sym0KindInference) ())
infixr 5 `C2Sym0`
type C2Sym1 :: T0 -> (~>) T2 T2
data C2Sym1 a0123456789876543210 a0123456789876543210
where
C2Sym1KindInference :: SameKind (Apply (C2Sym1 a0123456789876543210) arg) (C2Sym2 a0123456789876543210 arg) =>
C2Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (C2Sym1 a0123456789876543210) a0123456789876543210 = C2Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (C2Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) C2Sym1KindInference) ())
infixr 5 `C2Sym1`
type C2Sym2 (a0123456789876543210 :: T0) (a0123456789876543210 :: T2) =
C2 a0123456789876543210 a0123456789876543210 :: T2
infixr 5 `C2Sym2`
type (:||@#@$) :: (~>) T0 ((~>) T2 T2)
data (:||@#@$) a0123456789876543210
where
(::||@#@$###) :: SameKind (Apply (:||@#@$) arg) ((:||@#@$$) arg) =>
(:||@#@$) a0123456789876543210
type instance Apply (:||@#@$) a0123456789876543210 = (:||@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:||@#@$) where
suppressUnusedWarnings = snd (((,) (::||@#@$###)) ())
infixr 5 :||@#@$
type (:||@#@$$) :: T0 -> (~>) T2 T2
data (:||@#@$$) a0123456789876543210 a0123456789876543210
where
(::||@#@$$###) :: SameKind (Apply ((:||@#@$$) a0123456789876543210) arg) ((:||@#@$$$) a0123456789876543210 arg) =>
(:||@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:||@#@$$) a0123456789876543210) a0123456789876543210 = (:||@#@$$$) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:||@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::||@#@$$###)) ())
infixr 5 :||@#@$$
type (:||@#@$$$) (a0123456789876543210 :: T0) (a0123456789876543210 :: T2) =
(:||) a0123456789876543210 a0123456789876543210 :: T2
infixr 5 :||@#@$$$
infixr 5 :%||
infixr 5 `SC2`
data ST2 :: T2 -> GHC.Types.Type
where
SN2 :: ST2 (N2 :: T2)
SC2 :: forall (n :: T0) (n :: T2).
(Sing n) -> (Sing n) -> ST2 (C2 n n :: T2)
(:%||) :: forall (n :: T0) (n :: T2).
(Sing n) -> (Sing n) -> ST2 ((:||) n n :: T2)
type instance Sing @T2 = ST2
instance SingKind T2 where
type Demote T2 = T2
fromSing SN2 = N2
fromSing (SC2 b b) = (C2 (fromSing b)) (fromSing b)
fromSing ((:%||) b b) = ((:||) (fromSing b)) (fromSing b)
toSing N2 = SomeSing SN2
toSing (C2 (b :: Demote T0) (b :: Demote T2))
= case
((,) (toSing b :: SomeSing T0)) (toSing b :: SomeSing T2)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing ((SC2 c) c) }
toSing ((:||) (b :: Demote T0) (b :: Demote T2))
= case
((,) (toSing b :: SomeSing T0)) (toSing b :: SomeSing T2)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:%||) c) c) }
instance SingI N2 where
sing = SN2
instance (SingI n, SingI n) => SingI (C2 (n :: T0) (n :: T2)) where
sing = (SC2 sing) sing
instance SingI (C2Sym0 :: (~>) T0 ((~>) T2 T2)) where
sing = (singFun2 @C2Sym0) SC2
instance SingI d => SingI (C2Sym1 (d :: T0) :: (~>) T2 T2) where
sing = (singFun1 @(C2Sym1 (d :: T0))) (SC2 (sing @d))
instance (SingI n, SingI n) =>
SingI ((:||) (n :: T0) (n :: T2)) where
sing = ((:%||) sing) sing
instance SingI ((:||@#@$) :: (~>) T0 ((~>) T2 T2)) where
sing = (singFun2 @(:||@#@$)) (:%||)
instance SingI d =>
SingI ((:||@#@$$) (d :: T0) :: (~>) T2 T2) where
sing = (singFun1 @((:||@#@$$) (d :: T0))) ((:%||) (sing @d))