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 SX :: forall a. X a -> Type where SX1 :: SX X1 SX2 :: forall a (n :: Y a). (Sing (n :: Y a)) -> SX (X2 n) type instance Sing @(X a) = SX 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 SY :: forall a. Y a -> Type where SY1 :: SY Y1 SY2 :: forall a (n :: X a). (Sing (n :: X a)) -> SY (Y2 n) type instance Sing @(Y a) = SY 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 instance Data.Singletons.ShowSing.ShowSing (Y a) => Show (SX (z :: X a)) where showsPrec _ SX1 = showString "SX1" showsPrec p_0123456789876543210 (SX2 (arg_0123456789876543210 :: Sing argTy_0123456789876543210)) = (showParen (((>) p_0123456789876543210) 10)) (((.) (showString "SX2 ")) ((showsPrec 11) arg_0123456789876543210)) :: Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210 => ShowS instance Data.Singletons.ShowSing.ShowSing (X a) => Show (SY (z :: Y a)) where showsPrec _ SY1 = showString "SY1" showsPrec p_0123456789876543210 (SY2 (arg_0123456789876543210 :: Sing argTy_0123456789876543210)) = (showParen (((>) p_0123456789876543210) 10)) (((.) (showString "SY2 ")) ((showsPrec 11) arg_0123456789876543210)) :: Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210 => ShowS 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 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