singletons-2.5.1: tests/compile-and-dump/Singletons/T371.ghc86.template
Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| data Y (a :: Type)
= Y1 | Y2 (X a)
deriving Show
data X (a :: Type)
= X1 | X2 (Y a)
deriving Show |]
======>
data X (a :: Type)
= X1 | X2 (Y a)
deriving Show
data Y (a :: Type)
= Y1 | Y2 (X a)
deriving Show
type X1Sym0 = X1
type X2Sym1 (t0123456789876543210 :: Y a0123456789876543210) =
X2 t0123456789876543210
instance SuppressUnusedWarnings X2Sym0 where
suppressUnusedWarnings = snd (((,) X2Sym0KindInference) ())
data X2Sym0 :: forall (a0123456789876543210 :: Type).
(~>) (Y a0123456789876543210) (X (a0123456789876543210 :: Type))
where
X2Sym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
X2Sym0 t0123456789876543210
type instance Apply X2Sym0 t0123456789876543210 = X2 t0123456789876543210
type Y1Sym0 = Y1
type Y2Sym1 (t0123456789876543210 :: X a0123456789876543210) =
Y2 t0123456789876543210
instance SuppressUnusedWarnings Y2Sym0 where
suppressUnusedWarnings = snd (((,) Y2Sym0KindInference) ())
data Y2Sym0 :: forall (a0123456789876543210 :: Type).
(~>) (X a0123456789876543210) (Y (a0123456789876543210 :: Type))
where
Y2Sym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) =>
Y2Sym0 t0123456789876543210
type instance Apply Y2Sym0 t0123456789876543210 = Y2 t0123456789876543210
type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
ShowsPrec_0123456789876543210 _ X1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "X1") a_0123456789876543210
ShowsPrec_0123456789876543210 p_0123456789876543210 (X2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "X2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
a0123456789876543210
a0123456789876543210
arg. 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_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.
(~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. 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_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.
(~>) GHC.Types.Nat ((~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance PShow (X a) where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
ShowsPrec_0123456789876543210 _ Y1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "Y1") a_0123456789876543210
ShowsPrec_0123456789876543210 p_0123456789876543210 (Y2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Y2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
a0123456789876543210
a0123456789876543210
arg. 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_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.
(~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. 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_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.
(~>) GHC.Types.Nat ((~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance PShow (Y a) where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
data instance Sing :: X a -> Type
where
SX1 :: Sing X1
SX2 :: forall a (n :: Y a). (Sing (n :: Y a)) -> Sing (X2 n)
type SX = (Sing :: X a -> Type)
instance SingKind a => SingKind (X a) where
type Demote (X a) = X (Demote a)
fromSing SX1 = X1
fromSing (SX2 b) = X2 (fromSing b)
toSing X1 = SomeSing SX1
toSing (X2 (b :: Demote (Y a)))
= case toSing b :: SomeSing (Y a) of {
SomeSing c -> SomeSing (SX2 c) }
data instance Sing :: Y a -> Type
where
SY1 :: Sing Y1
SY2 :: forall a (n :: X a). (Sing (n :: X a)) -> Sing (Y2 n)
type SY = (Sing :: Y a -> Type)
instance SingKind a => SingKind (Y a) where
type Demote (Y a) = Y (Demote a)
fromSing SY1 = Y1
fromSing (SY2 b) = Y2 (fromSing b)
toSing Y1 = SomeSing SY1
toSing (Y2 (b :: Demote (X a)))
= case toSing b :: SomeSing (X a) of {
SomeSing c -> SomeSing (SY2 c) }
instance SShow (Y a) => SShow (X a) where
sShowsPrec ::
forall (t1 :: GHC.Types.Nat) (t2 :: X a) (t3 :: GHC.Types.Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (X a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SX1
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "X1")))
sA_0123456789876543210
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SX2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing
((applySing ((singFun3 @ShowParenSym0) sShowParen))
((applySing
((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "X2 "))))
((applySing
((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
sArg_0123456789876543210))))
sA_0123456789876543210
instance SShow (X a) => SShow (Y a) where
sShowsPrec ::
forall (t1 :: GHC.Types.Nat) (t2 :: Y a) (t3 :: GHC.Types.Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (Y a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SY1
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "Y1")))
sA_0123456789876543210
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SY2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing
((applySing ((singFun3 @ShowParenSym0) sShowParen))
((applySing
((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "Y2 "))))
((applySing
((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
sArg_0123456789876543210))))
sA_0123456789876543210
deriving instance Data.Singletons.ShowSing.ShowSing (Y a) =>
Show (Sing (z :: X a))
deriving instance Data.Singletons.ShowSing.ShowSing (X a) =>
Show (Sing (z :: Y a))
instance SingI X1 where
sing = SX1
instance SingI n => SingI (X2 (n :: Y a)) where
sing = SX2 sing
instance SingI (X2Sym0 :: (~>) (Y a) (X (a :: Type))) where
sing = (singFun1 @X2Sym0) SX2
instance SingI (TyCon1 X2 :: (~>) (Y a) (X (a :: Type))) where
sing = (singFun1 @(TyCon1 X2)) SX2
instance SingI Y1 where
sing = SY1
instance SingI n => SingI (Y2 (n :: X a)) where
sing = SY2 sing
instance SingI (Y2Sym0 :: (~>) (X a) (Y (a :: Type))) where
sing = (singFun1 @Y2Sym0) SY2
instance SingI (TyCon1 Y2 :: (~>) (X a) (Y (a :: Type))) where
sing = (singFun1 @(TyCon1 Y2)) SY2