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 = Zero
    type SuccSym1 (t0123456789876543210 :: Nat) =
        Succ t0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 t0123456789876543210
    type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
    type PredSym1 (a0123456789876543210 :: Nat) =
        Pred a0123456789876543210
    instance SuppressUnusedWarnings PredSym0 where
      suppressUnusedWarnings = snd (((,) PredSym0KindInference) ())
    data PredSym0 :: (~>) Nat Nat
      where
        PredSym0KindInference :: forall a0123456789876543210
                                        arg. SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
                                 PredSym0 a0123456789876543210
    type instance Apply PredSym0 a0123456789876543210 = Pred a0123456789876543210
    type PlusSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
        Plus a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (PlusSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) PlusSym1KindInference) ())
    data PlusSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        PlusSym1KindInference :: forall a0123456789876543210
                                        a0123456789876543210
                                        arg. SameKind (Apply (PlusSym1 a0123456789876543210) arg) (PlusSym2 a0123456789876543210 arg) =>
                                 PlusSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (PlusSym1 a0123456789876543210) a0123456789876543210 = Plus a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings = snd (((,) PlusSym0KindInference) ())
    data PlusSym0 :: (~>) Nat ((~>) Nat Nat)
      where
        PlusSym0KindInference :: forall a0123456789876543210
                                        arg. SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
                                 PlusSym0 a0123456789876543210
    type instance Apply PlusSym0 a0123456789876543210 = PlusSym1 a0123456789876543210
    type family Pred (a :: Nat) :: Nat where
      Pred Zero = ZeroSym0
      Pred (Succ n) = n
    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 family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (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) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Succ ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Nat) (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 :: Nat) :: (~>) 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) :: (~>) Nat ((~>) 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 :: (~>) GHC.Types.Nat ((~>) Nat ((~>) 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 Nat where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
      Compare_0123456789876543210 Zero (Succ _) = LTSym0
      Compare_0123456789876543210 (Succ _) Zero = GTSym0
    type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
        Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) Compare_0123456789876543210Sym1KindInference) ())
    data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering
      where
        Compare_0123456789876543210Sym1KindInference :: forall a0123456789876543210
                                                               a0123456789876543210
                                                               arg. 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_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) Compare_0123456789876543210Sym0KindInference) ())
    data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
      where
        Compare_0123456789876543210Sym0KindInference :: forall a0123456789876543210
                                                               arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
                                                        Compare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
    instance POrd Nat where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789876543210 Zero Zero = TrueSym0
      Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b
      Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0
    instance PEq Nat where
      type (==) a b = Equals_0123456789876543210 a b
    sPred ::
      forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t :: Nat)
    sPlus ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply PlusSym0 t) t :: Nat)
    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))
    data instance Sing :: Nat -> GHC.Types.Type
      where
        SZero :: Sing Zero
        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n)
    type SNat = (Sing :: Nat -> GHC.Types.Type)
    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 SShow Nat => SShow Nat where
      sShowsPrec ::
        forall (t1 :: GHC.Types.Nat) (t2 :: Nat) (t3 :: GHC.Types.Symbol).
        Sing t1
        -> Sing t2
           -> Sing t3
              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol))
                                                             -> GHC.Types.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))
                       (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
                ((applySing
                    ((applySing ((singFun3 @(.@#@$)) (%.)))
                       ((applySing ((singFun2 @ShowStringSym0) sShowString))
                          (sing :: Sing "Succ "))))
                   ((applySing
                       ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
                          (Data.Singletons.Prelude.Num.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)
                                                 -> GHC.Types.Type) t1) t2)
      sCompare SZero SZero
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            Data.Singletons.Prelude.Instances.SNil
      sCompare
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing
                    ((singFun2 @(:@#@$))
                       Data.Singletons.Prelude.Instances.SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               Data.Singletons.Prelude.Instances.SNil)
      sCompare SZero (SSucc _) = SLT
      sCompare (SSucc _) SZero = SGT
    instance SEq Nat => SEq Nat where
      (%==) SZero SZero = STrue
      (%==) SZero (SSucc _) = SFalse
      (%==) (SSucc _) SZero = SFalse
      (%==) (SSucc a) (SSucc b) = ((%==) a) b
    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 })
    deriving instance Data.Singletons.ShowSing.ShowSing Nat =>
                      Show (Sing (z :: Nat))
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance SingI (SuccSym0 :: (~>) Nat Nat) where
      sing = (singFun1 @SuccSym0) SSucc
    instance SingI (TyCon1 Succ :: (~>) Nat Nat) where
      sing = (singFun1 @(TyCon1 Succ)) SSucc