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 [] = [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))
    type Succ_0123456789876543210 :: [Bool] -> [Bool]
    type family Succ_0123456789876543210 (a :: [Bool]) :: [Bool] where
      Succ_0123456789876543210 '[] = Apply (Apply (:@#@$) TrueSym0) NilSym0
      Succ_0123456789876543210 ('(:) 'False as) = Apply (Apply (:@#@$) TrueSym0) as
      Succ_0123456789876543210 ('(:) 'True as) = Apply (Apply (:@#@$) FalseSym0) (Apply SuccSym0 as)
    type Succ_0123456789876543210Sym0 :: (~>) [Bool] [Bool]
    data Succ_0123456789876543210Sym0 :: (~>) [Bool] [Bool]
      where
        Succ_0123456789876543210Sym0KindInference :: SameKind (Apply Succ_0123456789876543210Sym0 arg) (Succ_0123456789876543210Sym1 arg) =>
                                                     Succ_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Succ_0123456789876543210Sym0 a0123456789876543210 = Succ_0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings Succ_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Succ_0123456789876543210Sym0KindInference ())
    type Succ_0123456789876543210Sym1 :: [Bool] -> [Bool]
    type family Succ_0123456789876543210Sym1 (a0123456789876543210 :: [Bool]) :: [Bool] where
      Succ_0123456789876543210Sym1 a0123456789876543210 = Succ_0123456789876543210 a0123456789876543210
    type Pred_0123456789876543210 :: [Bool] -> [Bool]
    type family Pred_0123456789876543210 (a :: [Bool]) :: [Bool] where
      Pred_0123456789876543210 '[] = Apply ErrorSym0 "pred 0"
      Pred_0123456789876543210 ('(:) 'False as) = Apply (Apply (:@#@$) TrueSym0) (Apply PredSym0 as)
      Pred_0123456789876543210 ('(:) 'True as) = Apply (Apply (:@#@$) FalseSym0) as
    type Pred_0123456789876543210Sym0 :: (~>) [Bool] [Bool]
    data Pred_0123456789876543210Sym0 :: (~>) [Bool] [Bool]
      where
        Pred_0123456789876543210Sym0KindInference :: SameKind (Apply Pred_0123456789876543210Sym0 arg) (Pred_0123456789876543210Sym1 arg) =>
                                                     Pred_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Pred_0123456789876543210Sym0 a0123456789876543210 = Pred_0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings Pred_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Pred_0123456789876543210Sym0KindInference ())
    type Pred_0123456789876543210Sym1 :: [Bool] -> [Bool]
    type family Pred_0123456789876543210Sym1 (a0123456789876543210 :: [Bool]) :: [Bool] where
      Pred_0123456789876543210Sym1 a0123456789876543210 = Pred_0123456789876543210 a0123456789876543210
    type family Case_0123456789876543210 i arg_0123456789876543210 t where
      Case_0123456789876543210 i arg_0123456789876543210 'True = NilSym0
      Case_0123456789876543210 i arg_0123456789876543210 'False = Apply SuccSym0 (Apply ToEnumSym0 (Apply PredSym0 i))
    type family Case_0123456789876543210 i arg_0123456789876543210 t where
      Case_0123456789876543210 i arg_0123456789876543210 'True = Apply ErrorSym0 "negative toEnum"
      Case_0123456789876543210 i arg_0123456789876543210 'False = Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (==@#@$) i) (FromInteger 0))
    type family Case_0123456789876543210 arg_0123456789876543210 t where
      Case_0123456789876543210 arg_0123456789876543210 i = Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (<@#@$) i) (FromInteger 0))
    type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural
                                       -> [Bool]
    type family ToEnum_0123456789876543210 (a :: GHC.Num.Natural.Natural) :: [Bool] where
      ToEnum_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210
    type ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural [Bool]
    data ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural [Bool]
      where
        ToEnum_0123456789876543210Sym0KindInference :: SameKind (Apply ToEnum_0123456789876543210Sym0 arg) (ToEnum_0123456789876543210Sym1 arg) =>
                                                       ToEnum_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ToEnum_0123456789876543210Sym0 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ToEnum_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) ToEnum_0123456789876543210Sym0KindInference ())
    type ToEnum_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
                                           -> [Bool]
    type family ToEnum_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: [Bool] where
      ToEnum_0123456789876543210Sym1 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
    type FromEnum_0123456789876543210 :: [Bool]
                                         -> GHC.Num.Natural.Natural
    type family FromEnum_0123456789876543210 (a :: [Bool]) :: GHC.Num.Natural.Natural where
      FromEnum_0123456789876543210 '[] = FromInteger 0
      FromEnum_0123456789876543210 ('(:) 'False as) = Apply (Apply (*@#@$) (FromInteger 2)) (Apply FromEnumSym0 as)
      FromEnum_0123456789876543210 ('(:) 'True as) = Apply (Apply (+@#@$) (FromInteger 1)) (Apply (Apply (*@#@$) (FromInteger 2)) (Apply FromEnumSym0 as))
    type FromEnum_0123456789876543210Sym0 :: (~>) [Bool] GHC.Num.Natural.Natural
    data FromEnum_0123456789876543210Sym0 :: (~>) [Bool] GHC.Num.Natural.Natural
      where
        FromEnum_0123456789876543210Sym0KindInference :: SameKind (Apply FromEnum_0123456789876543210Sym0 arg) (FromEnum_0123456789876543210Sym1 arg) =>
                                                         FromEnum_0123456789876543210Sym0 a0123456789876543210
    type instance Apply FromEnum_0123456789876543210Sym0 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings FromEnum_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) FromEnum_0123456789876543210Sym0KindInference ())
    type FromEnum_0123456789876543210Sym1 :: [Bool]
                                             -> GHC.Num.Natural.Natural
    type family FromEnum_0123456789876543210Sym1 (a0123456789876543210 :: [Bool]) :: GHC.Num.Natural.Natural where
      FromEnum_0123456789876543210Sym1 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
    instance PEnum [Bool] where
      type Succ a = Apply Succ_0123456789876543210Sym0 a
      type Pred a = Apply Pred_0123456789876543210Sym0 a
      type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a
      type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a
    instance SEnum [Bool] where
      sSucc ::
        forall (t :: [Bool]). Sing t
                              -> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool] -> Type) t)
      sPred ::
        forall (t :: [Bool]). Sing t
                              -> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool] -> Type) t)
      sToEnum ::
        forall (t :: GHC.Num.Natural.Natural). Sing t
                                               -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural [Bool]
                                                                             -> Type) t)
      sFromEnum ::
        forall (t :: [Bool]). Sing t
                              -> Sing (Apply (FromEnumSym0 :: TyFun [Bool] GHC.Num.Natural.Natural
                                                              -> Type) t)
      sSucc SNil
        = applySing (applySing (singFun2 @(:@#@$) SCons) STrue) SNil
      sSucc (SCons SFalse (sAs :: Sing as))
        = applySing (applySing (singFun2 @(:@#@$) SCons) STrue) sAs
      sSucc (SCons STrue (sAs :: Sing as))
        = applySing
            (applySing (singFun2 @(:@#@$) SCons) SFalse)
            (applySing (singFun1 @SuccSym0 sSucc) sAs)
      sPred SNil = sError (sing :: Sing "pred 0")
      sPred (SCons SFalse (sAs :: Sing as))
        = applySing
            (applySing (singFun2 @(:@#@$) SCons) STrue)
            (applySing (singFun1 @PredSym0 sPred) sAs)
      sPred (SCons STrue (sAs :: Sing as))
        = applySing (applySing (singFun2 @(:@#@$) SCons) SFalse) sAs
      sToEnum (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
        = id
            @(Sing (Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210))
            (case sArg_0123456789876543210 of
               (sI :: Sing i)
                 -> id
                      @(Sing (Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (<@#@$) i) (FromInteger 0))))
                      (case
                           applySing
                             (applySing (singFun2 @(<@#@$) (%<)) sI)
                             (sFromInteger (sing :: Sing 0))
                       of
                         STrue -> sError (sing :: Sing "negative toEnum")
                         SFalse
                           -> id
                                @(Sing (Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (==@#@$) i) (FromInteger 0))))
                                (case
                                     applySing
                                       (applySing (singFun2 @(==@#@$) (%==)) sI)
                                       (sFromInteger (sing :: Sing 0))
                                 of
                                   STrue -> SNil
                                   SFalse
                                     -> applySing
                                          (singFun1 @SuccSym0 sSucc)
                                          (applySing
                                             (singFun1 @ToEnumSym0 sToEnum)
                                             (applySing (singFun1 @PredSym0 sPred) sI)))))
      sFromEnum SNil = sFromInteger (sing :: Sing 0)
      sFromEnum (SCons SFalse (sAs :: Sing as))
        = applySing
            (applySing
               (singFun2 @(*@#@$) (%*)) (sFromInteger (sing :: Sing 2)))
            (applySing (singFun1 @FromEnumSym0 sFromEnum) sAs)
      sFromEnum (SCons STrue (sAs :: Sing as))
        = applySing
            (applySing
               (singFun2 @(+@#@$) (%+)) (sFromInteger (sing :: Sing 1)))
            (applySing
               (applySing
                  (singFun2 @(*@#@$) (%*)) (sFromInteger (sing :: Sing 2)))
               (applySing (singFun1 @FromEnumSym0 sFromEnum) sAs))