singletons-base-3.3: tests/compile-and-dump/Singletons/DataValues.golden
Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| pr = Pair (Succ Zero) ([Zero])
complex = Pair (Pair (Just Zero) Zero) False
tuple = (False, Just Zero, True)
aList = [Zero, Succ Zero, Succ (Succ Zero)]
data Pair a b
= Pair a b
deriving Show |]
======>
data Pair a b
= Pair a b
deriving Show
pr = Pair (Succ Zero) [Zero]
complex = Pair (Pair (Just Zero) Zero) False
tuple = (False, Just Zero, True)
aList = [Zero, Succ Zero, Succ (Succ Zero)]
type PairSym0 :: forall a b. (~>) a ((~>) b (Pair a b))
data PairSym0 :: (~>) a ((~>) b (Pair a b))
where
PairSym0KindInference :: SameKind (Apply PairSym0 arg) (PairSym1 arg) =>
PairSym0 a0123456789876543210
type instance Apply PairSym0 a0123456789876543210 = PairSym1 a0123456789876543210
instance SuppressUnusedWarnings PairSym0 where
suppressUnusedWarnings = snd ((,) PairSym0KindInference ())
type PairSym1 :: forall a b. a -> (~>) b (Pair a b)
data PairSym1 (a0123456789876543210 :: a) :: (~>) b (Pair a b)
where
PairSym1KindInference :: SameKind (Apply (PairSym1 a0123456789876543210) arg) (PairSym2 a0123456789876543210 arg) =>
PairSym1 a0123456789876543210 a0123456789876543210
type instance Apply (PairSym1 a0123456789876543210) a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (PairSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) PairSym1KindInference ())
type PairSym2 :: forall a b. a -> b -> Pair a b
type family PairSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where
PairSym2 a0123456789876543210 a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
type family AListSym0 where
AListSym0 = AList
type family TupleSym0 where
TupleSym0 = Tuple
type family ComplexSym0 where
ComplexSym0 = Complex
type family PrSym0 where
PrSym0 = Pr
type family AList where
AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
type family Tuple where
Tuple = Apply (Apply (Apply Tuple3Sym0 FalseSym0) (Apply JustSym0 ZeroSym0)) TrueSym0
type family Complex where
Complex = Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
type family Pr where
Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0)
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> Pair a b -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> (~>) (Pair a b) ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) (Pair a b) ((~>) Symbol Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-> Pair a b -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) :: (~>) Symbol Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-> Pair a b -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow (Pair a b) where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
sAList :: Sing @_ AListSym0
sTuple :: Sing @_ TupleSym0
sComplex :: Sing @_ ComplexSym0
sPr :: Sing @_ PrSym0
sAList
= applySing
(applySing (singFun2 @(:@#@$) SCons) SZero)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing (singFun1 @SuccSym0 SSucc) SZero))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(singFun1 @SuccSym0 SSucc)
(applySing (singFun1 @SuccSym0 SSucc) SZero)))
SNil))
sTuple
= applySing
(applySing
(applySing (singFun3 @Tuple3Sym0 STuple3) SFalse)
(applySing (singFun1 @JustSym0 SJust) SZero))
STrue
sComplex
= applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing (singFun1 @JustSym0 SJust) SZero))
SZero))
SFalse
sPr
= applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing (singFun1 @SuccSym0 SSucc) SZero))
(applySing (applySing (singFun2 @(:@#@$) SCons) SZero) SNil)
data SPair :: forall a b. Pair a b -> Type
where
SPair :: forall a b (n :: a) (n :: b).
(Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b)
type instance Sing @(Pair a b) = SPair
instance (SingKind a, SingKind b) => SingKind (Pair a b) where
type Demote (Pair a b) = Pair (Demote a) (Demote b)
fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
toSing (Pair (b :: Demote a) (b :: Demote b))
= case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
instance (SShow a, SShow b) => SShow (Pair a b) where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: Pair a b)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
(sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 10))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Pair ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.)) (singFun1 @ShowSpaceSym0 sShowSpace))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210)))))
sA_0123456789876543210
deriving instance (Data.Singletons.ShowSing.ShowSing a,
Data.Singletons.ShowSing.ShowSing b) =>
Show (SPair (z :: Pair a b))
instance (SingI n, SingI n) => SingI (Pair (n :: a) (n :: b)) where
sing = SPair sing sing
instance SingI n => SingI1 (Pair (n :: a)) where
liftSing = SPair sing
instance SingI2 Pair where
liftSing2 = SPair
instance SingI (PairSym0 :: (~>) a ((~>) b (Pair a b))) where
sing = singFun2 @PairSym0 SPair
instance SingI d =>
SingI (PairSym1 (d :: a) :: (~>) b (Pair a b)) where
sing = singFun1 @(PairSym1 (d :: a)) (SPair (sing @d))
instance SingI1 (PairSym1 :: a -> (~>) b (Pair a b)) where
liftSing (s :: Sing (d :: a))
= singFun1 @(PairSym1 (d :: a)) (SPair s)