Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| plus :: Nat -> Nat -> Nat
          plus Zero m = m
          plus (Succ n) m = Succ (plus n m)
          pred :: Nat -> Nat
          pred Zero = Zero
          pred (Succ n) = n
          
          data Nat
            where
              Zero :: Nat
              Succ :: Nat -> Nat
            deriving (Eq, Show, Read, Ord) |]
  ======>
    data Nat
      where
        Zero :: Nat
        Succ :: Nat -> Nat
      deriving (Eq, Show, Read, Ord)
    plus :: Nat -> Nat -> Nat
    plus Zero m = m
    plus (Succ n) m = Succ (plus n m)
    pred :: Nat -> Nat
    pred Zero = Zero
    pred (Succ n) = n
    type ZeroSym0 :: Nat
    type family ZeroSym0 :: Nat where
      ZeroSym0 = Zero
    type SuccSym0 :: (~>) Nat Nat
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 a0123456789876543210
    type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd ((,) SuccSym0KindInference ())
    type SuccSym1 :: Nat -> Nat
    type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where
      SuccSym1 a0123456789876543210 = Succ a0123456789876543210
    type PredSym0 :: (~>) Nat Nat
    data PredSym0 :: (~>) Nat Nat
      where
        PredSym0KindInference :: SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
                                 PredSym0 a0123456789876543210
    type instance Apply PredSym0 a0123456789876543210 = Pred a0123456789876543210
    instance SuppressUnusedWarnings PredSym0 where
      suppressUnusedWarnings = snd ((,) PredSym0KindInference ())
    type PredSym1 :: Nat -> Nat
    type family PredSym1 (a0123456789876543210 :: Nat) :: Nat where
      PredSym1 a0123456789876543210 = Pred a0123456789876543210
    type PlusSym0 :: (~>) Nat ((~>) Nat Nat)
    data PlusSym0 :: (~>) Nat ((~>) Nat Nat)
      where
        PlusSym0KindInference :: SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
                                 PlusSym0 a0123456789876543210
    type instance Apply PlusSym0 a0123456789876543210 = PlusSym1 a0123456789876543210
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings = snd ((,) PlusSym0KindInference ())
    type PlusSym1 :: Nat -> (~>) Nat Nat
    data PlusSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        PlusSym1KindInference :: SameKind (Apply (PlusSym1 a0123456789876543210) arg) (PlusSym2 a0123456789876543210 arg) =>
                                 PlusSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (PlusSym1 a0123456789876543210) a0123456789876543210 = Plus a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (PlusSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) PlusSym1KindInference ())
    type PlusSym2 :: Nat -> Nat -> Nat
    type family PlusSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      PlusSym2 a0123456789876543210 a0123456789876543210 = Plus a0123456789876543210 a0123456789876543210
    type Pred :: Nat -> Nat
    type family Pred (a :: Nat) :: Nat where
      Pred Zero = ZeroSym0
      Pred (Succ n) = n
    type Plus :: Nat -> Nat -> Nat
    type family Plus (a :: Nat) (a :: Nat) :: Nat where
      Plus Zero m = m
      Plus (Succ n) m = Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
    type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool
    type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where
      TFHelper_0123456789876543210 Zero Zero = TrueSym0
      TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0
      TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0
      TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210
    type TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool)
    data TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool)
      where
        TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
                                                         TFHelper_0123456789876543210Sym0 a0123456789876543210
    type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
    type TFHelper_0123456789876543210Sym1 :: Nat -> (~>) Nat Bool
    data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
      where
        TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                         TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
    type TFHelper_0123456789876543210Sym2 :: Nat -> Nat -> Bool
    type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Bool where
      TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PEq Nat where
      type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
    type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
                                          -> Nat -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Nat) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 _ Zero a_0123456789876543210 = Apply (Apply ShowStringSym0 "Zero") a_0123456789876543210
      ShowsPrec_0123456789876543210 p_0123456789876543210 (Succ arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Succ ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol))
    data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.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
                                              -> (~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol)
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) Nat ((~>) GHC.Types.Symbol GHC.Types.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
                                              -> Nat -> (~>) GHC.Types.Symbol GHC.Types.Symbol
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Nat) :: (~>) GHC.Types.Symbol GHC.Types.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
                                              -> Nat -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Nat) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PShow Nat where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
    type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
      Compare_0123456789876543210 Zero (Succ _) = LTSym0
      Compare_0123456789876543210 (Succ _) Zero = GTSym0
    type Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
    data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
      where
        Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
                                                        Compare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym0KindInference ())
    type Compare_0123456789876543210Sym1 :: Nat -> (~>) Nat Ordering
    data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering
      where
        Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                        Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym1KindInference ())
    type Compare_0123456789876543210Sym2 :: Nat -> Nat -> Ordering
    type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Ordering where
      Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance POrd Nat where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    sPred ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply PredSym0 t :: Nat) :: Type)
    sPlus ::
      (forall (t :: Nat) (t :: Nat).
       Sing t
       -> Sing t -> Sing (Apply (Apply PlusSym0 t) t :: Nat) :: Type)
    sPred SZero = SZero
    sPred (SSucc (sN :: Sing n)) = sN
    sPlus SZero (sM :: Sing m) = sM
    sPlus (SSucc (sN :: Sing n)) (sM :: Sing m)
      = applySing
          (singFun1 @SuccSym0 SSucc)
          (applySing (applySing (singFun2 @PlusSym0 sPlus) sN) sM)
    instance SingI (PredSym0 :: (~>) Nat Nat) where
      sing = singFun1 @PredSym0 sPred
    instance SingI (PlusSym0 :: (~>) Nat ((~>) Nat Nat)) where
      sing = singFun2 @PlusSym0 sPlus
    instance SingI d =>
             SingI (PlusSym1 (d :: Nat) :: (~>) Nat Nat) where
      sing = singFun1 @(PlusSym1 (d :: Nat)) (sPlus (sing @d))
    instance SingI1 (PlusSym1 :: Nat -> (~>) Nat Nat) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(PlusSym1 (d :: Nat)) (sPlus s)
    data SNat :: Nat -> Type
      where
        SZero :: SNat (Zero :: Nat)
        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
    type instance Sing @Nat = SNat
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ (b :: Demote Nat))
        = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
    instance SEq Nat => SEq Nat where
      (%==) ::
        forall (t1 :: Nat) (t2 :: Nat). Sing t1
                                        -> Sing t2
                                           -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool)
                                                                              -> Type) t1) t2)
      (%==) SZero SZero = STrue
      (%==) SZero (SSucc _) = SFalse
      (%==) (SSucc _) SZero = SFalse
      (%==)
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = applySing
            (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
            sB_0123456789876543210
    instance SShow Nat => SShow Nat where
      sShowsPrec ::
        forall (t1 :: GHC.Num.Natural.Natural)
               (t2 :: Nat)
               (t3 :: GHC.Types.Symbol). Sing t1
                                         -> Sing t2
                                            -> Sing t3
                                               -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol))
                                                                                              -> Type) t1) t2) t3)
      sShowsPrec
        _
        SZero
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Zero"))
            sA_0123456789876543210
      sShowsPrec
        (sP_0123456789876543210 :: Sing p_0123456789876543210)
        (SSucc (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 "Succ ")))
                  (applySing
                     (applySing
                        (singFun3 @ShowsPrecSym0 sShowsPrec)
                        (sFromInteger (sing :: Sing 11)))
                     sArg_0123456789876543210)))
            sA_0123456789876543210
    instance SOrd Nat => SOrd Nat where
      sCompare ::
        forall (t1 :: Nat) (t2 :: Nat). Sing t1
                                        -> Sing t2
                                           -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
                                                                                 -> Type) t1) t2)
      sCompare SZero SZero
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            (applySing
               (applySing
                  (singFun2 @(:@#@$) SCons)
                  (applySing
                     (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
                     sB_0123456789876543210))
               SNil)
      sCompare SZero (SSucc _) = SLT
      sCompare (SSucc _) SZero = SGT
    instance SDecide Nat => SDecide Nat where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _) = Disproved (\ x -> case x of {})
      (%~) (SSucc _) SZero = Disproved (\ x -> case x of {})
      (%~) (SSucc a) (SSucc b)
        = case (%~) a b of
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of Refl -> contra Refl)
    instance SDecide Nat =>
             Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where
      Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance SDecide Nat =>
             Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where
      Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    deriving instance Data.Singletons.ShowSing.ShowSing Nat =>
                      Show (SNat (z :: Nat))
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance SingI1 Succ where
      liftSing = SSucc
    instance SingI (SuccSym0 :: (~>) Nat Nat) where
      sing = singFun1 @SuccSym0 SSucc