T371.golden

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 :: forall (a :: Type). X a
    type family X1Sym0 @(a :: Type) :: X a where
      X1Sym0 = X1
    type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X a)
    data X2Sym0 :: (~>) (Y a) (X a)
      where
        X2Sym0KindInference :: SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
                               X2Sym0 a0123456789876543210
    type instance Apply @(Y a) @(X a) X2Sym0 a0123456789876543210 = X2 a0123456789876543210
    instance SuppressUnusedWarnings X2Sym0 where
      suppressUnusedWarnings = snd ((,) X2Sym0KindInference ())
    type X2Sym1 :: forall (a :: Type). Y a -> X a
    type family X2Sym1 @(a :: Type) (a0123456789876543210 :: Y a) :: X a where
      X2Sym1 a0123456789876543210 = X2 a0123456789876543210
    type Y1Sym0 :: forall (a :: Type). Y a
    type family Y1Sym0 @(a :: Type) :: Y a where
      Y1Sym0 = Y1
    type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y a)
    data Y2Sym0 :: (~>) (X a) (Y a)
      where
        Y2Sym0KindInference :: SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) =>
                               Y2Sym0 a0123456789876543210
    type instance Apply @(X a) @(Y a) Y2Sym0 a0123456789876543210 = Y2 a0123456789876543210
    instance SuppressUnusedWarnings Y2Sym0 where
      suppressUnusedWarnings = snd ((,) Y2Sym0KindInference ())
    type Y2Sym1 :: forall (a :: Type). X a -> Y a
    type family Y2Sym1 @(a :: Type) (a0123456789876543210 :: X a) :: Y a where
      Y2Sym1 a0123456789876543210 = Y2 a0123456789876543210
    type ShowsPrec_0123456789876543210 :: forall a. GHC.Num.Natural.Natural
                                                    -> X a -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 @a (_ :: GHC.Num.Natural.Natural) (X1 :: X a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply ShowStringSym0 "X1") a_0123456789876543210
      ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) (X2 arg_0123456789876543210 :: X a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "X2 ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    instance PShow (X a) where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    type ShowsPrec_0123456789876543210 :: forall a. GHC.Num.Natural.Natural
                                                    -> Y a -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 @a (_ :: GHC.Num.Natural.Natural) (Y1 :: Y a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply ShowStringSym0 "Y1") a_0123456789876543210
      ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Y2 arg_0123456789876543210 :: Y a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Y2 ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    instance PShow (Y a) where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    data SX :: forall (a :: Type). X a -> Type
      where
        SX1 :: forall (a :: Type). SX (X1 :: X a)
        SX2 :: forall (a :: Type) (n :: Y a). (Sing n) -> SX (X2 n :: X a)
    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)))
        = (\cases (SomeSing c) -> SomeSing (SX2 c))
            (toSing b :: SomeSing (Y a))
    data SY :: forall (a :: Type). Y a -> Type
      where
        SY1 :: forall (a :: Type). SY (Y1 :: Y a)
        SY2 :: forall (a :: Type) (n :: X a). (Sing n) -> SY (Y2 n :: Y a)
    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)))
        = (\cases (SomeSing c) -> SomeSing (SY2 c))
            (toSing b :: SomeSing (X a))
    instance SShow (Y a) => SShow (X a) where
      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)
                     (sFromInteger (sing :: Sing 10))))
               (applySing
                  (applySing
                     (singFun3 @(.@#@$) (%.))
                     (applySing
                        (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "X2 ")))
                  (applySing
                     (applySing
                        (singFun3 @ShowsPrecSym0 sShowsPrec)
                        (sFromInteger (sing :: Sing 11)))
                     sArg_0123456789876543210)))
            sA_0123456789876543210
    instance SShow (X a) => SShow (Y a) where
      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)
                     (sFromInteger (sing :: Sing 10))))
               (applySing
                  (applySing
                     (singFun3 @(.@#@$) (%.))
                     (applySing
                        (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Y2 ")))
                  (applySing
                     (applySing
                        (singFun3 @ShowsPrecSym0 sShowsPrec)
                        (sFromInteger (sing :: Sing 11)))
                     sArg_0123456789876543210)))
            sA_0123456789876543210
    deriving instance Data.Singletons.ShowSing.ShowSing (Y a) =>
                      Show (SX (z :: X a))
    deriving instance Data.Singletons.ShowSing.ShowSing (X a) =>
                      Show (SY (z :: Y a))
    instance SingI X1 where
      sing = SX1
    instance SingI n => SingI (X2 (n :: Y a)) where
      sing = SX2 sing
    instance SingI1 X2 where
      liftSing = SX2
    instance SingI (X2Sym0 :: (~>) (Y a) (X a)) where
      sing = singFun1 @X2Sym0 SX2
    instance SingI Y1 where
      sing = SY1
    instance SingI n => SingI (Y2 (n :: X a)) where
      sing = SY2 sing
    instance SingI1 Y2 where
      liftSing = SY2
    instance SingI (Y2Sym0 :: (~>) (X a) (Y a)) where
      sing = singFun1 @Y2Sym0 SY2