Singletons/T136.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| instance Enum BiNat where
            succ [] = [True]
            succ (False : as) = True : as
            succ (True : as) = False : succ as
            pred [] = error "pred 0"
            pred (False : as) = True : pred as
            pred (True : as) = False : as
            toEnum i
              | i < 0 = error "negative toEnum"
              | i == 0 = []
              | otherwise = succ (toEnum (pred i))
            fromEnum [] = 0
            fromEnum (False : as) = 2 * fromEnum as
            fromEnum (True : as) = 1 + 2 * fromEnum as |]
  ======>
    instance Enum BiNat where
      succ GHC.Types.[] = [True]
      succ (False GHC.Types.: as) = (True GHC.Types.: as)
      succ (True GHC.Types.: as) = (False GHC.Types.: (succ as))
      pred GHC.Types.[] = error "pred 0"
      pred (False GHC.Types.: as) = (True GHC.Types.: (pred as))
      pred (True GHC.Types.: as) = (False GHC.Types.: as)
      toEnum i
        | (i < 0) = error "negative toEnum"
        | (i == 0) = []
        | otherwise = succ (toEnum (pred i))
      fromEnum GHC.Types.[] = 0
      fromEnum (False GHC.Types.: as) = (2 * (fromEnum as))
      fromEnum (True GHC.Types.: as) = (1 + (2 * (fromEnum as)))
    type family Succ_0123456789 (a :: [Bool]) :: [Bool] where
      Succ_0123456789 '[] = Apply (Apply (:$) TrueSym0) '[]
      Succ_0123456789 ((:) False as) = Apply (Apply (:$) TrueSym0) as
      Succ_0123456789 ((:) True as) = Apply (Apply (:$) FalseSym0) (Apply SuccSym0 as)
    type Succ_0123456789Sym1 (t :: [Bool]) = Succ_0123456789 t
    instance SuppressUnusedWarnings Succ_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Succ_0123456789Sym0KindInference GHC.Tuple.())
    data Succ_0123456789Sym0 (l :: TyFun [Bool] [Bool])
      = forall arg. KindOf (Apply Succ_0123456789Sym0 arg) ~ KindOf (Succ_0123456789Sym1 arg) =>
        Succ_0123456789Sym0KindInference
    type instance Apply Succ_0123456789Sym0 l = Succ_0123456789Sym1 l
    type family Pred_0123456789 (a :: [Bool]) :: [Bool] where
      Pred_0123456789 '[] = Apply ErrorSym0 "pred 0"
      Pred_0123456789 ((:) False as) = Apply (Apply (:$) TrueSym0) (Apply PredSym0 as)
      Pred_0123456789 ((:) True as) = Apply (Apply (:$) FalseSym0) as
    type Pred_0123456789Sym1 (t :: [Bool]) = Pred_0123456789 t
    instance SuppressUnusedWarnings Pred_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Pred_0123456789Sym0KindInference GHC.Tuple.())
    data Pred_0123456789Sym0 (l :: TyFun [Bool] [Bool])
      = forall arg. KindOf (Apply Pred_0123456789Sym0 arg) ~ KindOf (Pred_0123456789Sym1 arg) =>
        Pred_0123456789Sym0KindInference
    type instance Apply Pred_0123456789Sym0 l = Pred_0123456789Sym1 l
    type family Case_0123456789 i arg_0123456789 t where
      Case_0123456789 i arg_0123456789 True = '[]
      Case_0123456789 i arg_0123456789 False = Apply SuccSym0 (Apply ToEnumSym0 (Apply PredSym0 i))
    type family Case_0123456789 i arg_0123456789 t where
      Case_0123456789 i arg_0123456789 True = Apply ErrorSym0 "negative toEnum"
      Case_0123456789 i arg_0123456789 False = Case_0123456789 i arg_0123456789 (Apply (Apply (:==$) i) (FromInteger 0))
    type family Case_0123456789 arg_0123456789 t where
      Case_0123456789 arg_0123456789 i = Case_0123456789 i arg_0123456789 (Apply (Apply (:<$) i) (FromInteger 0))
    type family ToEnum_0123456789 (a :: GHC.TypeLits.Nat) :: [Bool] where
      ToEnum_0123456789 arg_0123456789 = Case_0123456789 arg_0123456789 arg_0123456789
    type ToEnum_0123456789Sym1 (t :: GHC.TypeLits.Nat) =
        ToEnum_0123456789 t
    instance SuppressUnusedWarnings ToEnum_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) ToEnum_0123456789Sym0KindInference GHC.Tuple.())
    data ToEnum_0123456789Sym0 (l :: TyFun GHC.TypeLits.Nat [Bool])
      = forall arg. KindOf (Apply ToEnum_0123456789Sym0 arg) ~ KindOf (ToEnum_0123456789Sym1 arg) =>
        ToEnum_0123456789Sym0KindInference
    type instance Apply ToEnum_0123456789Sym0 l = ToEnum_0123456789Sym1 l
    type family FromEnum_0123456789 (a :: [Bool]) :: GHC.TypeLits.Nat where
      FromEnum_0123456789 '[] = FromInteger 0
      FromEnum_0123456789 ((:) False as) = Apply (Apply (:*$) (FromInteger 2)) (Apply FromEnumSym0 as)
      FromEnum_0123456789 ((:) True as) = Apply (Apply (:+$) (FromInteger 1)) (Apply (Apply (:*$) (FromInteger 2)) (Apply FromEnumSym0 as))
    type FromEnum_0123456789Sym1 (t :: [Bool]) = FromEnum_0123456789 t
    instance SuppressUnusedWarnings FromEnum_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) FromEnum_0123456789Sym0KindInference GHC.Tuple.())
    data FromEnum_0123456789Sym0 (l :: TyFun [Bool] GHC.TypeLits.Nat)
      = forall arg. KindOf (Apply FromEnum_0123456789Sym0 arg) ~ KindOf (FromEnum_0123456789Sym1 arg) =>
        FromEnum_0123456789Sym0KindInference
    type instance Apply FromEnum_0123456789Sym0 l = FromEnum_0123456789Sym1 l
    instance PEnum (KProxy :: KProxy [Bool]) where
      type Succ (a :: [Bool]) = Apply Succ_0123456789Sym0 a
      type Pred (a :: [Bool]) = Apply Pred_0123456789Sym0 a
      type ToEnum (a :: GHC.TypeLits.Nat) = Apply ToEnum_0123456789Sym0 a
      type FromEnum (a :: [Bool]) = Apply FromEnum_0123456789Sym0 a
    instance SEnum (KProxy :: KProxy [Bool]) where
      sSucc ::
        forall (t0 :: [Bool]).
        Sing t0
        -> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool] -> *) t0 :: [Bool])
      sPred ::
        forall (t0 :: [Bool]).
        Sing t0
        -> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool] -> *) t0 :: [Bool])
      sToEnum ::
        forall (t0 :: GHC.TypeLits.Nat).
        Sing t0
        -> Sing (Apply (ToEnumSym0 :: TyFun GHC.TypeLits.Nat [Bool]
                                      -> *) t0 :: [Bool])
      sFromEnum ::
        forall (t0 :: [Bool]).
        Sing t0
        -> Sing (Apply (FromEnumSym0 :: TyFun [Bool] GHC.TypeLits.Nat
                                        -> *) t0 :: GHC.TypeLits.Nat)
      sSucc SNil
        = let
            lambda :: t0 ~ '[] => Sing (Apply SuccSym0 t0 :: [Bool])
            lambda
              = applySing
                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue) SNil
          in lambda
      sSucc (SCons SFalse sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) FalseSym0) as =>
              Sing as -> Sing (Apply SuccSym0 t0 :: [Bool])
            lambda as
              = applySing
                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue) as
          in lambda sAs
      sSucc (SCons STrue sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) TrueSym0) as =>
              Sing as -> Sing (Apply SuccSym0 t0 :: [Bool])
            lambda as
              = applySing
                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) SFalse)
                  (applySing (singFun1 (Proxy :: Proxy SuccSym0) sSucc) as)
          in lambda sAs
      sPred SNil
        = let
            lambda :: t0 ~ '[] => Sing (Apply PredSym0 t0 :: [Bool])
            lambda = sError (sing :: Sing "pred 0")
          in lambda
      sPred (SCons SFalse sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) FalseSym0) as =>
              Sing as -> Sing (Apply PredSym0 t0 :: [Bool])
            lambda as
              = applySing
                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue)
                  (applySing (singFun1 (Proxy :: Proxy PredSym0) sPred) as)
          in lambda sAs
      sPred (SCons STrue sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) TrueSym0) as =>
              Sing as -> Sing (Apply PredSym0 t0 :: [Bool])
            lambda as
              = applySing
                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) SFalse) as
          in lambda sAs
      sToEnum sArg_0123456789
        = let
            lambda ::
              forall arg_0123456789. t0 ~ arg_0123456789 =>
              Sing arg_0123456789 -> Sing (Apply ToEnumSym0 t0 :: [Bool])
            lambda arg_0123456789
              = case arg_0123456789 of {
                  sI
                    -> let
                         lambda ::
                           forall i. i ~ arg_0123456789 =>
                           Sing i -> Sing (Case_0123456789 arg_0123456789 i :: [Bool])
                         lambda i
                           = case
                                 applySing
                                   (applySing (singFun2 (Proxy :: Proxy (:<$)) (%:<)) i)
                                   (sFromInteger (sing :: Sing 0))
                             of {
                               STrue
                                 -> let
                                      lambda ::
                                        TrueSym0 ~ Apply (Apply (:<$) i) (FromInteger 0) =>
                                        Sing (Case_0123456789 i arg_0123456789 TrueSym0 :: [Bool])
                                      lambda = sError (sing :: Sing "negative toEnum")
                                    in lambda
                               SFalse
                                 -> let
                                      lambda ::
                                        FalseSym0 ~ Apply (Apply (:<$) i) (FromInteger 0) =>
                                        Sing (Case_0123456789 i arg_0123456789 FalseSym0 :: [Bool])
                                      lambda
                                        = case
                                              applySing
                                                (applySing
                                                   (singFun2 (Proxy :: Proxy (:==$)) (%:==)) i)
                                                (sFromInteger (sing :: Sing 0))
                                          of {
                                            STrue
                                              -> let
                                                   lambda ::
                                                     TrueSym0 ~ Apply (Apply (:==$) i) (FromInteger 0) =>
                                                     Sing (Case_0123456789 i arg_0123456789 TrueSym0 :: [Bool])
                                                   lambda = SNil
                                                 in lambda
                                            SFalse
                                              -> let
                                                   lambda ::
                                                     FalseSym0 ~ Apply (Apply (:==$) i) (FromInteger 0) =>
                                                     Sing (Case_0123456789 i arg_0123456789 FalseSym0 :: [Bool])
                                                   lambda
                                                     = applySing
                                                         (singFun1 (Proxy :: Proxy SuccSym0) sSucc)
                                                         (applySing
                                                            (singFun1
                                                               (Proxy :: Proxy ToEnumSym0) sToEnum)
                                                            (applySing
                                                               (singFun1
                                                                  (Proxy :: Proxy PredSym0) sPred)
                                                               i))
                                                 in lambda } ::
                                            Sing (Case_0123456789 i arg_0123456789 (Apply (Apply (:==$) i) (FromInteger 0)) :: [Bool])
                                    in lambda } ::
                               Sing (Case_0123456789 i arg_0123456789 (Apply (Apply (:<$) i) (FromInteger 0)) :: [Bool])
                       in lambda sI } ::
                  Sing (Case_0123456789 arg_0123456789 arg_0123456789 :: [Bool])
          in lambda sArg_0123456789
      sFromEnum SNil
        = let
            lambda ::
              t0 ~ '[] => Sing (Apply FromEnumSym0 t0 :: GHC.TypeLits.Nat)
            lambda = sFromInteger (sing :: Sing 0)
          in lambda
      sFromEnum (SCons SFalse sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) FalseSym0) as =>
              Sing as -> Sing (Apply FromEnumSym0 t0 :: GHC.TypeLits.Nat)
            lambda as
              = applySing
                  (applySing
                     (singFun2 (Proxy :: Proxy (:*$)) (%:*))
                     (sFromInteger (sing :: Sing 2)))
                  (applySing (singFun1 (Proxy :: Proxy FromEnumSym0) sFromEnum) as)
          in lambda sAs
      sFromEnum (SCons STrue sAs)
        = let
            lambda ::
              forall as. t0 ~ Apply (Apply (:$) TrueSym0) as =>
              Sing as -> Sing (Apply FromEnumSym0 t0 :: GHC.TypeLits.Nat)
            lambda as
              = applySing
                  (applySing
                     (singFun2 (Proxy :: Proxy (:+$)) (%:+))
                     (sFromInteger (sing :: Sing 1)))
                  (applySing
                     (applySing
                        (singFun2 (Proxy :: Proxy (:*$)) (%:*))
                        (sFromInteger (sing :: Sing 2)))
                     (applySing (singFun1 (Proxy :: Proxy FromEnumSym0) sFromEnum) as))
          in lambda sAs