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 (t :: Nat) = Succ t
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
    data SuccSym0 (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = Succ l
    type PredSym1 (t :: Nat) = Pred t
    instance SuppressUnusedWarnings PredSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) PredSym0KindInference) GHC.Tuple.())
    data PredSym0 (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
        PredSym0KindInference
    type instance Apply PredSym0 l = Pred l
    type PlusSym2 (t :: Nat) (t :: Nat) = Plus t t
    instance SuppressUnusedWarnings PlusSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) PlusSym1KindInference) GHC.Tuple.())
    data PlusSym1 (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply (PlusSym1 l) arg) (PlusSym2 l arg) =>
        PlusSym1KindInference
    type instance Apply (PlusSym1 l) l = Plus l l
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) PlusSym0KindInference) GHC.Tuple.())
    data PlusSym0 (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
      = forall arg. SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
        PlusSym0KindInference
    type instance Apply PlusSym0 l = PlusSym1 l
    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 (t :: GHC.Types.Nat) (t :: Nat) (t :: GHC.Types.Symbol) =
        ShowsPrec_0123456789876543210 t t t
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym2 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym2KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym2 (l :: GHC.Types.Nat) (l :: Nat) (l :: TyFun GHC.Types.Symbol GHC.Types.Symbol)
      = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 l l) arg) (ShowsPrec_0123456789876543210Sym3 l l arg) =>
        ShowsPrec_0123456789876543210Sym2KindInference
    type instance Apply (ShowsPrec_0123456789876543210Sym2 l l) l = ShowsPrec_0123456789876543210 l l l
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym1 (l :: GHC.Types.Nat) (l :: TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
                                                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 l) arg) (ShowsPrec_0123456789876543210Sym2 l arg) =>
        ShowsPrec_0123456789876543210Sym1KindInference
    type instance Apply (ShowsPrec_0123456789876543210Sym1 l) l = ShowsPrec_0123456789876543210Sym2 l l
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym0 (l :: TyFun GHC.Types.Nat (TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
                                                                                 -> GHC.Types.Type)
                                                                      -> GHC.Types.Type))
      = forall arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
        ShowsPrec_0123456789876543210Sym0KindInference
    type instance Apply ShowsPrec_0123456789876543210Sym0 l = ShowsPrec_0123456789876543210Sym1 l
    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 (t :: Nat) (t :: Nat) =
        Compare_0123456789876543210 t t
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym1 (l :: Nat) (l :: TyFun Nat Ordering)
      = forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
        Compare_0123456789876543210Sym1KindInference
    type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym0 (l :: TyFun Nat (TyFun Nat Ordering
                                                          -> GHC.Types.Type))
      = forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
        Compare_0123456789876543210Sym0KindInference
    type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
    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)
    data instance Sing (z :: Nat)
      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 (TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
                                                                                             -> GHC.Types.Type)
                                                                                  -> GHC.Types.Type)
                                                             -> 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 (TyFun Nat Ordering
                                                            -> GHC.Types.Type)
                                                 -> 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 })
    instance Data.Singletons.ShowSing.ShowSing Nat =>
             Data.Singletons.ShowSing.ShowSing Nat where
      Data.Singletons.ShowSing.showsSingPrec _ SZero = showString "SZero"
      Data.Singletons.ShowSing.showsSingPrec
        p_0123456789876543210
        (SSucc arg_0123456789876543210)
        = (showParen (((>) p_0123456789876543210) 10))
            (((.) (showString "SSucc "))
               ((Data.Singletons.ShowSing.showsSingPrec 11)
                  arg_0123456789876543210))
    instance Data.Singletons.ShowSing.ShowSing Nat =>
             Show (Sing (z :: Nat)) where
      showsPrec = Data.Singletons.ShowSing.showsSingPrec
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing