singletons-base-3.5: tests/compile-and-dump/Singletons/ShowDeriving.golden
Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| infixl 5 `MkFoo2b`, :*:, :&:
data Foo1
= MkFoo1
deriving Show
data Foo2 a
= MkFoo2a a a | a `MkFoo2b` a | (:*:) a a | a :&: a
deriving Show
data Foo3
= MkFoo3 {getFoo3a :: Bool, (***) :: Bool}
deriving Show |]
======>
data Foo1
= MkFoo1
deriving Show
infixl 5 `MkFoo2b`
infixl 5 :*:
infixl 5 :&:
data Foo2 a
= MkFoo2a a a | a `MkFoo2b` a | (:*:) a a | a :&: a
deriving Show
data Foo3
= MkFoo3 {getFoo3a :: Bool, (***) :: Bool}
deriving Show
type MkFoo1Sym0 :: Foo1
type family MkFoo1Sym0 :: Foo1 where
MkFoo1Sym0 = MkFoo1
type MkFoo2aSym0 :: forall a. (~>) a ((~>) a (Foo2 a))
data MkFoo2aSym0 :: (~>) a ((~>) a (Foo2 a))
where
MkFoo2aSym0KindInference :: SameKind (Apply MkFoo2aSym0 arg) (MkFoo2aSym1 arg) =>
MkFoo2aSym0 a0123456789876543210
type instance Apply @a @((~>) a (Foo2 a)) MkFoo2aSym0 a0123456789876543210 = MkFoo2aSym1 a0123456789876543210
instance SuppressUnusedWarnings MkFoo2aSym0 where
suppressUnusedWarnings = snd ((,) MkFoo2aSym0KindInference ())
type MkFoo2aSym1 :: forall a. a -> (~>) a (Foo2 a)
data MkFoo2aSym1 (a0123456789876543210 :: a) :: (~>) a (Foo2 a)
where
MkFoo2aSym1KindInference :: SameKind (Apply (MkFoo2aSym1 a0123456789876543210) arg) (MkFoo2aSym2 a0123456789876543210 arg) =>
MkFoo2aSym1 a0123456789876543210 a0123456789876543210
type instance Apply @a @(Foo2 a) (MkFoo2aSym1 a0123456789876543210) a0123456789876543210 = MkFoo2a a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MkFoo2aSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MkFoo2aSym1KindInference ())
type MkFoo2aSym2 :: forall a. a -> a -> Foo2 a
type family MkFoo2aSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where
MkFoo2aSym2 a0123456789876543210 a0123456789876543210 = MkFoo2a a0123456789876543210 a0123456789876543210
type MkFoo2bSym0 :: forall a. (~>) a ((~>) a (Foo2 a))
data MkFoo2bSym0 :: (~>) a ((~>) a (Foo2 a))
where
MkFoo2bSym0KindInference :: SameKind (Apply MkFoo2bSym0 arg) (MkFoo2bSym1 arg) =>
MkFoo2bSym0 a0123456789876543210
type instance Apply @a @((~>) a (Foo2 a)) MkFoo2bSym0 a0123456789876543210 = MkFoo2bSym1 a0123456789876543210
instance SuppressUnusedWarnings MkFoo2bSym0 where
suppressUnusedWarnings = snd ((,) MkFoo2bSym0KindInference ())
infixl 5 type `MkFoo2bSym0`
type MkFoo2bSym1 :: forall a. a -> (~>) a (Foo2 a)
data MkFoo2bSym1 (a0123456789876543210 :: a) :: (~>) a (Foo2 a)
where
MkFoo2bSym1KindInference :: SameKind (Apply (MkFoo2bSym1 a0123456789876543210) arg) (MkFoo2bSym2 a0123456789876543210 arg) =>
MkFoo2bSym1 a0123456789876543210 a0123456789876543210
type instance Apply @a @(Foo2 a) (MkFoo2bSym1 a0123456789876543210) a0123456789876543210 = MkFoo2b a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MkFoo2bSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MkFoo2bSym1KindInference ())
infixl 5 type `MkFoo2bSym1`
type MkFoo2bSym2 :: forall a. a -> a -> Foo2 a
type family MkFoo2bSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where
MkFoo2bSym2 a0123456789876543210 a0123456789876543210 = MkFoo2b a0123456789876543210 a0123456789876543210
infixl 5 type `MkFoo2bSym2`
type (:*:@#@$) :: forall a. (~>) a ((~>) a (Foo2 a))
data (:*:@#@$) :: (~>) a ((~>) a (Foo2 a))
where
(::*:@#@$###) :: SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) =>
(:*:@#@$) a0123456789876543210
type instance Apply @a @((~>) a (Foo2 a)) (:*:@#@$) a0123456789876543210 = (:*:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:*:@#@$) where
suppressUnusedWarnings = snd ((,) (::*:@#@$###) ())
infixl 5 type :*:@#@$
type (:*:@#@$$) :: forall a. a -> (~>) a (Foo2 a)
data (:*:@#@$$) (a0123456789876543210 :: a) :: (~>) a (Foo2 a)
where
(::*:@#@$$###) :: SameKind (Apply ((:*:@#@$$) a0123456789876543210) arg) ((:*:@#@$$$) a0123456789876543210 arg) =>
(:*:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply @a @(Foo2 a) ((:*:@#@$$) a0123456789876543210) a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:*:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ())
infixl 5 type :*:@#@$$
type (:*:@#@$$$) :: forall a. a -> a -> Foo2 a
type family (:*:@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where
(:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
infixl 5 type :*:@#@$$$
type (:&:@#@$) :: forall a. (~>) a ((~>) a (Foo2 a))
data (:&:@#@$) :: (~>) a ((~>) a (Foo2 a))
where
(::&:@#@$###) :: SameKind (Apply (:&:@#@$) arg) ((:&:@#@$$) arg) =>
(:&:@#@$) a0123456789876543210
type instance Apply @a @((~>) a (Foo2 a)) (:&:@#@$) a0123456789876543210 = (:&:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:&:@#@$) where
suppressUnusedWarnings = snd ((,) (::&:@#@$###) ())
infixl 5 type :&:@#@$
type (:&:@#@$$) :: forall a. a -> (~>) a (Foo2 a)
data (:&:@#@$$) (a0123456789876543210 :: a) :: (~>) a (Foo2 a)
where
(::&:@#@$$###) :: SameKind (Apply ((:&:@#@$$) a0123456789876543210) arg) ((:&:@#@$$$) a0123456789876543210 arg) =>
(:&:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply @a @(Foo2 a) ((:&:@#@$$) a0123456789876543210) a0123456789876543210 = (:&:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:&:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (::&:@#@$$###) ())
infixl 5 type :&:@#@$$
type (:&:@#@$$$) :: forall a. a -> a -> Foo2 a
type family (:&:@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where
(:&:@#@$$$) a0123456789876543210 a0123456789876543210 = (:&:) a0123456789876543210 a0123456789876543210
infixl 5 type :&:@#@$$$
type MkFoo3Sym0 :: (~>) Bool ((~>) Bool Foo3)
data MkFoo3Sym0 :: (~>) Bool ((~>) Bool Foo3)
where
MkFoo3Sym0KindInference :: SameKind (Apply MkFoo3Sym0 arg) (MkFoo3Sym1 arg) =>
MkFoo3Sym0 a0123456789876543210
type instance Apply @Bool @((~>) Bool Foo3) MkFoo3Sym0 a0123456789876543210 = MkFoo3Sym1 a0123456789876543210
instance SuppressUnusedWarnings MkFoo3Sym0 where
suppressUnusedWarnings = snd ((,) MkFoo3Sym0KindInference ())
type MkFoo3Sym1 :: Bool -> (~>) Bool Foo3
data MkFoo3Sym1 (a0123456789876543210 :: Bool) :: (~>) Bool Foo3
where
MkFoo3Sym1KindInference :: SameKind (Apply (MkFoo3Sym1 a0123456789876543210) arg) (MkFoo3Sym2 a0123456789876543210 arg) =>
MkFoo3Sym1 a0123456789876543210 a0123456789876543210
type instance Apply @Bool @Foo3 (MkFoo3Sym1 a0123456789876543210) a0123456789876543210 = MkFoo3 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MkFoo3Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MkFoo3Sym1KindInference ())
type MkFoo3Sym2 :: Bool -> Bool -> Foo3
type family MkFoo3Sym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Bool) :: Foo3 where
MkFoo3Sym2 a0123456789876543210 a0123456789876543210 = MkFoo3 a0123456789876543210 a0123456789876543210
type (***@#@$) :: (~>) Foo3 Bool
data (***@#@$) :: (~>) Foo3 Bool
where
(:***@#@$###) :: SameKind (Apply (***@#@$) arg) ((***@#@$$) arg) =>
(***@#@$) a0123456789876543210
type instance Apply @Foo3 @Bool (***@#@$) a0123456789876543210 = (***) a0123456789876543210
instance SuppressUnusedWarnings (***@#@$) where
suppressUnusedWarnings = snd ((,) (:***@#@$###) ())
type (***@#@$$) :: Foo3 -> Bool
type family (***@#@$$) (a0123456789876543210 :: Foo3) :: Bool where
(***@#@$$) a0123456789876543210 = (***) a0123456789876543210
type GetFoo3aSym0 :: (~>) Foo3 Bool
data GetFoo3aSym0 :: (~>) Foo3 Bool
where
GetFoo3aSym0KindInference :: SameKind (Apply GetFoo3aSym0 arg) (GetFoo3aSym1 arg) =>
GetFoo3aSym0 a0123456789876543210
type instance Apply @Foo3 @Bool GetFoo3aSym0 a0123456789876543210 = GetFoo3a a0123456789876543210
instance SuppressUnusedWarnings GetFoo3aSym0 where
suppressUnusedWarnings = snd ((,) GetFoo3aSym0KindInference ())
type GetFoo3aSym1 :: Foo3 -> Bool
type family GetFoo3aSym1 (a0123456789876543210 :: Foo3) :: Bool where
GetFoo3aSym1 a0123456789876543210 = GetFoo3a a0123456789876543210
type (***) :: Foo3 -> Bool
type family (***) (a :: Foo3) :: Bool where
(***) (MkFoo3 _ field) = field
type GetFoo3a :: Foo3 -> Bool
type family GetFoo3a (a :: Foo3) :: Bool where
GetFoo3a (MkFoo3 field _) = field
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> Foo1 -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Foo1) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ MkFoo1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "MkFoo1") a_0123456789876543210
instance PShow Foo1 where
type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
type ShowsPrec_0123456789876543210 :: forall a. GHC.Num.Natural.Natural
-> Foo2 a -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Foo2 a) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) (MkFoo2a arg_0123456789876543210 arg_0123456789876543210 :: Foo2 a) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "MkFoo2a ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) (MkFoo2b argL_0123456789876543210 argR_0123456789876543210 :: Foo2 a) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 5))) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argL_0123456789876543210)) (Apply (Apply (.@#@$) (Apply ShowStringSym0 " `MkFoo2b` ")) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argR_0123456789876543210)))) a_0123456789876543210
ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) ((:*:) arg_0123456789876543210 arg_0123456789876543210 :: Foo2 a) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "(:*:) ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) ((:&:) argL_0123456789876543210 argR_0123456789876543210 :: Foo2 a) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 5))) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argL_0123456789876543210)) (Apply (Apply (.@#@$) (Apply ShowStringSym0 " :&: ")) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argR_0123456789876543210)))) a_0123456789876543210
instance PShow (Foo2 a) where
type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> Foo3 -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Foo3) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 p_0123456789876543210 (MkFoo3 arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "MkFoo3 ")) (Apply (Apply (.@#@$) (Apply ShowCharSym0 '{')) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "getFoo3a = ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 0)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowCommaSpaceSym0) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "(***) = ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 0)) arg_0123456789876543210)) (Apply ShowCharSym0 '}'))))))))) a_0123456789876543210
instance PShow Foo3 where
type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
infixl 5 data :%&:
infixl 5 data :%*:
infixl 5 data `SMkFoo2b`
(%***) ::
(forall (t :: Foo3). Sing t -> Sing ((***) t :: Bool) :: Type)
sGetFoo3a ::
(forall (t :: Foo3). Sing t -> Sing (GetFoo3a t :: Bool) :: Type)
(%***) (SMkFoo3 _ (sField :: Sing field)) = sField
sGetFoo3a (SMkFoo3 (sField :: Sing field) _) = sField
instance SingI ((***@#@$) :: (~>) Foo3 Bool) where
sing = singFun1 @(***@#@$) (%***)
instance SingI (GetFoo3aSym0 :: (~>) Foo3 Bool) where
sing = singFun1 @GetFoo3aSym0 sGetFoo3a
data SFoo1 :: Foo1 -> Type where SMkFoo1 :: SFoo1 (MkFoo1 :: Foo1)
type instance Sing @Foo1 = SFoo1
instance SingKind Foo1 where
type Demote Foo1 = Foo1
fromSing SMkFoo1 = MkFoo1
toSing MkFoo1 = SomeSing SMkFoo1
data SFoo2 :: forall a. Foo2 a -> Type
where
SMkFoo2a :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SFoo2 (MkFoo2a n n :: Foo2 a)
SMkFoo2b :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SFoo2 (MkFoo2b n n :: Foo2 a)
(:%*:) :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SFoo2 ((:*:) n n :: Foo2 a)
(:%&:) :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SFoo2 ((:&:) n n :: Foo2 a)
type instance Sing @(Foo2 a) = SFoo2
instance SingKind a => SingKind (Foo2 a) where
type Demote (Foo2 a) = Foo2 (Demote a)
fromSing (SMkFoo2a b b) = MkFoo2a (fromSing b) (fromSing b)
fromSing (SMkFoo2b b b) = MkFoo2b (fromSing b) (fromSing b)
fromSing ((:%*:) b b) = (:*:) (fromSing b) (fromSing b)
fromSing ((:%&:) b b) = (:&:) (fromSing b) (fromSing b)
toSing (MkFoo2a (b :: Demote a) (b :: Demote a))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SMkFoo2a c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing a)
toSing (MkFoo2b (b :: Demote a) (b :: Demote a))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SMkFoo2b c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing a)
toSing ((:*:) (b :: Demote a) (b :: Demote a))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%*:) c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing a)
toSing ((:&:) (b :: Demote a) (b :: Demote a))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%&:) c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing a)
data SFoo3 :: Foo3 -> Type
where
SMkFoo3 :: forall (n :: Bool) (n :: Bool).
(Sing n) -> (Sing n) -> SFoo3 (MkFoo3 n n :: Foo3)
type instance Sing @Foo3 = SFoo3
instance SingKind Foo3 where
type Demote Foo3 = Foo3
fromSing (SMkFoo3 b b) = MkFoo3 (fromSing b) (fromSing b)
toSing (MkFoo3 (b :: Demote Bool) (b :: Demote Bool))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SMkFoo3 c c))
(toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
instance SShow Foo1 where
sShowsPrec
_
SMkFoo1
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "MkFoo1"))
sA_0123456789876543210
instance SShow a => SShow (Foo2 a) where
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SMkFoo2a (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 "MkFoo2a ")))
(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
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SMkFoo2b (sArgL_0123456789876543210 :: Sing argL_0123456789876543210)
(sArgR_0123456789876543210 :: Sing argR_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 5))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 6)))
sArgL_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString)
(sing :: Sing " `MkFoo2b` ")))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 6)))
sArgR_0123456789876543210))))
sA_0123456789876543210
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
((:%*:) (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 "(:*:) ")))
(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
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
((:%&:) (sArgL_0123456789876543210 :: Sing argL_0123456789876543210)
(sArgR_0123456789876543210 :: Sing argR_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 5))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 6)))
sArgL_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing " :&: ")))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 6)))
sArgR_0123456789876543210))))
sA_0123456789876543210
instance SShow Bool => SShow Foo3 where
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SMkFoo3 (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 "MkFoo3 ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing (singFun2 @ShowCharSym0 sShowChar) (sing :: Sing '{')))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString)
(sing :: Sing "getFoo3a = ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 0)))
sArg_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(singFun1 @ShowCommaSpaceSym0 sShowCommaSpace))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString)
(sing :: Sing "(***) = ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 0)))
sArg_0123456789876543210))
(applySing
(singFun2 @ShowCharSym0 sShowChar)
(sing :: Sing '}'))))))))))
sA_0123456789876543210
deriving instance Show (SFoo1 (z :: Foo1))
deriving instance Data.Singletons.ShowSing.ShowSing a =>
Show (SFoo2 (z :: Foo2 a))
deriving instance Data.Singletons.ShowSing.ShowSing Bool =>
Show (SFoo3 (z :: Foo3))
instance SingI MkFoo1 where
sing = SMkFoo1
instance (SingI n, SingI n) =>
SingI (MkFoo2a (n :: a) (n :: a)) where
sing = SMkFoo2a sing sing
instance SingI n => SingI1 (MkFoo2a (n :: a)) where
liftSing = SMkFoo2a sing
instance SingI2 MkFoo2a where
liftSing2 = SMkFoo2a
instance SingI (MkFoo2aSym0 :: (~>) a ((~>) a (Foo2 a))) where
sing = singFun2 @MkFoo2aSym0 SMkFoo2a
instance SingI d =>
SingI (MkFoo2aSym1 (d :: a) :: (~>) a (Foo2 a)) where
sing = singFun1 @(MkFoo2aSym1 (d :: a)) (SMkFoo2a (sing @d))
instance SingI1 (MkFoo2aSym1 :: a -> (~>) a (Foo2 a)) where
liftSing (s :: Sing (d :: a))
= singFun1 @(MkFoo2aSym1 (d :: a)) (SMkFoo2a s)
instance (SingI n, SingI n) =>
SingI (MkFoo2b (n :: a) (n :: a)) where
sing = SMkFoo2b sing sing
instance SingI n => SingI1 (MkFoo2b (n :: a)) where
liftSing = SMkFoo2b sing
instance SingI2 MkFoo2b where
liftSing2 = SMkFoo2b
instance SingI (MkFoo2bSym0 :: (~>) a ((~>) a (Foo2 a))) where
sing = singFun2 @MkFoo2bSym0 SMkFoo2b
instance SingI d =>
SingI (MkFoo2bSym1 (d :: a) :: (~>) a (Foo2 a)) where
sing = singFun1 @(MkFoo2bSym1 (d :: a)) (SMkFoo2b (sing @d))
instance SingI1 (MkFoo2bSym1 :: a -> (~>) a (Foo2 a)) where
liftSing (s :: Sing (d :: a))
= singFun1 @(MkFoo2bSym1 (d :: a)) (SMkFoo2b s)
instance (SingI n, SingI n) =>
SingI ((:*:) (n :: a) (n :: a)) where
sing = (:%*:) sing sing
instance SingI n => SingI1 ((:*:) (n :: a)) where
liftSing = (:%*:) sing
instance SingI2 (:*:) where
liftSing2 = (:%*:)
instance SingI ((:*:@#@$) :: (~>) a ((~>) a (Foo2 a))) where
sing = singFun2 @(:*:@#@$) (:%*:)
instance SingI d =>
SingI ((:*:@#@$$) (d :: a) :: (~>) a (Foo2 a)) where
sing = singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) (sing @d))
instance SingI1 ((:*:@#@$$) :: a -> (~>) a (Foo2 a)) where
liftSing (s :: Sing (d :: a))
= singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) s)
instance (SingI n, SingI n) =>
SingI ((:&:) (n :: a) (n :: a)) where
sing = (:%&:) sing sing
instance SingI n => SingI1 ((:&:) (n :: a)) where
liftSing = (:%&:) sing
instance SingI2 (:&:) where
liftSing2 = (:%&:)
instance SingI ((:&:@#@$) :: (~>) a ((~>) a (Foo2 a))) where
sing = singFun2 @(:&:@#@$) (:%&:)
instance SingI d =>
SingI ((:&:@#@$$) (d :: a) :: (~>) a (Foo2 a)) where
sing = singFun1 @((:&:@#@$$) (d :: a)) ((:%&:) (sing @d))
instance SingI1 ((:&:@#@$$) :: a -> (~>) a (Foo2 a)) where
liftSing (s :: Sing (d :: a))
= singFun1 @((:&:@#@$$) (d :: a)) ((:%&:) s)
instance (SingI n, SingI n) =>
SingI (MkFoo3 (n :: Bool) (n :: Bool)) where
sing = SMkFoo3 sing sing
instance SingI n => SingI1 (MkFoo3 (n :: Bool)) where
liftSing = SMkFoo3 sing
instance SingI2 MkFoo3 where
liftSing2 = SMkFoo3
instance SingI (MkFoo3Sym0 :: (~>) Bool ((~>) Bool Foo3)) where
sing = singFun2 @MkFoo3Sym0 SMkFoo3
instance SingI d =>
SingI (MkFoo3Sym1 (d :: Bool) :: (~>) Bool Foo3) where
sing = singFun1 @(MkFoo3Sym1 (d :: Bool)) (SMkFoo3 (sing @d))
instance SingI1 (MkFoo3Sym1 :: Bool -> (~>) Bool Foo3) where
liftSing (s :: Sing (d :: Bool))
= singFun1 @(MkFoo3Sym1 (d :: Bool)) (SMkFoo3 s)