singletons-base-3.5: tests/compile-and-dump/Singletons/T159.golden
Singletons/T159.hs:0:0:: Splicing declarations
genSingletons [''T0, ''T1]
======>
type ASym0 :: T0
type family ASym0 :: T0 where
ASym0 = 'A
type BSym0 :: T0
type family BSym0 :: T0 where
BSym0 = 'B
type CSym0 :: T0
type family CSym0 :: T0 where
CSym0 = 'C
type DSym0 :: T0
type family DSym0 :: T0 where
DSym0 = 'D
type ESym0 :: T0
type family ESym0 :: T0 where
ESym0 = 'E
type FSym0 :: T0
type family FSym0 :: T0 where
FSym0 = 'F
type ST0 :: T0 -> Type
data ST0 :: T0 -> Type
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 :: T1
type family N1Sym0 :: T1 where
N1Sym0 = 'N1
type C1Sym0 :: (~>) T0 ((~>) T1 T1)
data C1Sym0 :: (~>) T0 ((~>) T1 T1)
where
C1Sym0KindInference :: SameKind (Apply C1Sym0 arg) (C1Sym1 arg) =>
C1Sym0 a0123456789876543210
type instance Apply @T0 @((~>) T1 T1) C1Sym0 a0123456789876543210 = C1Sym1 a0123456789876543210
instance SuppressUnusedWarnings C1Sym0 where
suppressUnusedWarnings = snd ((,) C1Sym0KindInference ())
infixr 5 type `C1Sym0`
type C1Sym1 :: T0 -> (~>) T1 T1
data C1Sym1 (a0123456789876543210 :: T0) :: (~>) T1 T1
where
C1Sym1KindInference :: SameKind (Apply (C1Sym1 a0123456789876543210) arg) (C1Sym2 a0123456789876543210 arg) =>
C1Sym1 a0123456789876543210 a0123456789876543210
type instance Apply @T1 @T1 (C1Sym1 a0123456789876543210) a0123456789876543210 = 'C1 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (C1Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) C1Sym1KindInference ())
infixr 5 type `C1Sym1`
type C1Sym2 :: T0 -> T1 -> T1
type family C1Sym2 (a0123456789876543210 :: T0) (a0123456789876543210 :: T1) :: T1 where
C1Sym2 a0123456789876543210 a0123456789876543210 = 'C1 a0123456789876543210 a0123456789876543210
infixr 5 type `C1Sym2`
type (:&&@#@$) :: (~>) T0 ((~>) T1 T1)
data (:&&@#@$) :: (~>) T0 ((~>) T1 T1)
where
(::&&@#@$###) :: SameKind (Apply (:&&@#@$) arg) ((:&&@#@$$) arg) =>
(:&&@#@$) a0123456789876543210
type instance Apply @T0 @((~>) T1 T1) (:&&@#@$) a0123456789876543210 = (:&&@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:&&@#@$) where
suppressUnusedWarnings = snd ((,) (::&&@#@$###) ())
infixr 5 type :&&@#@$
type (:&&@#@$$) :: T0 -> (~>) T1 T1
data (:&&@#@$$) (a0123456789876543210 :: T0) :: (~>) T1 T1
where
(::&&@#@$$###) :: SameKind (Apply ((:&&@#@$$) a0123456789876543210) arg) ((:&&@#@$$$) a0123456789876543210 arg) =>
(:&&@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply @T1 @T1 ((:&&@#@$$) a0123456789876543210) a0123456789876543210 = '(:&&) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:&&@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (::&&@#@$$###) ())
infixr 5 type :&&@#@$$
type (:&&@#@$$$) :: T0 -> T1 -> T1
type family (:&&@#@$$$) (a0123456789876543210 :: T0) (a0123456789876543210 :: T1) :: T1 where
(:&&@#@$$$) a0123456789876543210 a0123456789876543210 = '(:&&) a0123456789876543210 a0123456789876543210
infixr 5 type :&&@#@$$$
type ST1 :: T1 -> Type
data ST1 :: T1 -> Type
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))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SC1 c c))
(toSing b :: SomeSing T0) (toSing b :: SomeSing T1)
toSing ((:&&) (b :: Demote T0) (b :: Demote T1))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%&&) c c))
(toSing b :: SomeSing T0) (toSing b :: SomeSing T1)
infixr 5 data `SC1`
infixr 5 data :%&&
instance SingI 'N1 where
sing = SN1
instance (SingI n, SingI n) =>
SingI ('C1 (n :: T0) (n :: T1)) where
sing = SC1 sing sing
instance SingI n => SingI1 ('C1 (n :: T0)) where
liftSing = SC1 sing
instance SingI2 'C1 where
liftSing2 = SC1
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 SingI1 (C1Sym1 :: T0 -> (~>) T1 T1) where
liftSing (s :: Sing (d :: T0))
= singFun1 @(C1Sym1 (d :: T0)) (SC1 s)
instance (SingI n, SingI n) =>
SingI ('(:&&) (n :: T0) (n :: T1)) where
sing = (:%&&) sing sing
instance SingI n => SingI1 ('(:&&) (n :: T0)) where
liftSing = (:%&&) sing
instance SingI2 '(:&&) where
liftSing2 = (:%&&)
instance SingI ((:&&@#@$) :: (~>) T0 ((~>) T1 T1)) where
sing = singFun2 @(:&&@#@$) (:%&&)
instance SingI d =>
SingI ((:&&@#@$$) (d :: T0) :: (~>) T1 T1) where
sing = singFun1 @((:&&@#@$$) (d :: T0)) ((:%&&) (sing @d))
instance SingI1 ((:&&@#@$$) :: T0 -> (~>) T1 T1) where
liftSing (s :: Sing (d :: T0))
= singFun1 @((:&&@#@$$) (d :: T0)) ((:%&&) s)
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 :: T2
type family N2Sym0 :: T2 where
N2Sym0 = N2
type C2Sym0 :: (~>) T0 ((~>) T2 T2)
data C2Sym0 :: (~>) T0 ((~>) T2 T2)
where
C2Sym0KindInference :: SameKind (Apply C2Sym0 arg) (C2Sym1 arg) =>
C2Sym0 a0123456789876543210
type instance Apply @T0 @((~>) T2 T2) C2Sym0 a0123456789876543210 = C2Sym1 a0123456789876543210
instance SuppressUnusedWarnings C2Sym0 where
suppressUnusedWarnings = snd ((,) C2Sym0KindInference ())
infixr 5 type `C2Sym0`
type C2Sym1 :: T0 -> (~>) T2 T2
data C2Sym1 (a0123456789876543210 :: T0) :: (~>) T2 T2
where
C2Sym1KindInference :: SameKind (Apply (C2Sym1 a0123456789876543210) arg) (C2Sym2 a0123456789876543210 arg) =>
C2Sym1 a0123456789876543210 a0123456789876543210
type instance Apply @T2 @T2 (C2Sym1 a0123456789876543210) a0123456789876543210 = C2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (C2Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) C2Sym1KindInference ())
infixr 5 type `C2Sym1`
type C2Sym2 :: T0 -> T2 -> T2
type family C2Sym2 (a0123456789876543210 :: T0) (a0123456789876543210 :: T2) :: T2 where
C2Sym2 a0123456789876543210 a0123456789876543210 = C2 a0123456789876543210 a0123456789876543210
infixr 5 type `C2Sym2`
type (:||@#@$) :: (~>) T0 ((~>) T2 T2)
data (:||@#@$) :: (~>) T0 ((~>) T2 T2)
where
(::||@#@$###) :: SameKind (Apply (:||@#@$) arg) ((:||@#@$$) arg) =>
(:||@#@$) a0123456789876543210
type instance Apply @T0 @((~>) T2 T2) (:||@#@$) a0123456789876543210 = (:||@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:||@#@$) where
suppressUnusedWarnings = snd ((,) (::||@#@$###) ())
infixr 5 type :||@#@$
type (:||@#@$$) :: T0 -> (~>) T2 T2
data (:||@#@$$) (a0123456789876543210 :: T0) :: (~>) T2 T2
where
(::||@#@$$###) :: SameKind (Apply ((:||@#@$$) a0123456789876543210) arg) ((:||@#@$$$) a0123456789876543210 arg) =>
(:||@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply @T2 @T2 ((:||@#@$$) a0123456789876543210) a0123456789876543210 = (:||) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:||@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (::||@#@$$###) ())
infixr 5 type :||@#@$$
type (:||@#@$$$) :: T0 -> T2 -> T2
type family (:||@#@$$$) (a0123456789876543210 :: T0) (a0123456789876543210 :: T2) :: T2 where
(:||@#@$$$) a0123456789876543210 a0123456789876543210 = (:||) a0123456789876543210 a0123456789876543210
infixr 5 type :||@#@$$$
infixr 5 data :%||
infixr 5 data `SC2`
data ST2 :: T2 -> 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))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SC2 c c))
(toSing b :: SomeSing T0) (toSing b :: SomeSing T2)
toSing ((:||) (b :: Demote T0) (b :: Demote T2))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%||) c c))
(toSing b :: SomeSing T0) (toSing b :: SomeSing T2)
instance SingI N2 where
sing = SN2
instance (SingI n, SingI n) => SingI (C2 (n :: T0) (n :: T2)) where
sing = SC2 sing sing
instance SingI n => SingI1 (C2 (n :: T0)) where
liftSing = SC2 sing
instance SingI2 C2 where
liftSing2 = SC2
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 SingI1 (C2Sym1 :: T0 -> (~>) T2 T2) where
liftSing (s :: Sing (d :: T0))
= singFun1 @(C2Sym1 (d :: T0)) (SC2 s)
instance (SingI n, SingI n) =>
SingI ((:||) (n :: T0) (n :: T2)) where
sing = (:%||) sing sing
instance SingI n => SingI1 ((:||) (n :: T0)) where
liftSing = (:%||) sing
instance SingI2 (:||) where
liftSing2 = (:%||)
instance SingI ((:||@#@$) :: (~>) T0 ((~>) T2 T2)) where
sing = singFun2 @(:||@#@$) (:%||)
instance SingI d =>
SingI ((:||@#@$$) (d :: T0) :: (~>) T2 T2) where
sing = singFun1 @((:||@#@$$) (d :: T0)) ((:%||) (sing @d))
instance SingI1 ((:||@#@$$) :: T0 -> (~>) T2 T2) where
liftSing (s :: Sing (d :: T0))
= singFun1 @((:||@#@$$) (d :: T0)) ((:%||) s)