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)