Singletons/LambdasComprehensive.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| foo :: [Nat]
          foo
            = map (\ x -> either_ pred Succ x) [Left Zero, Right (Succ Zero)]
          bar :: [Nat]
          bar = map (either_ pred Succ) [Left Zero, Right (Succ Zero)] |]
  ======>
    foo :: [Nat]
    foo
      = map (\ x -> either_ pred Succ x) [Left Zero, Right (Succ Zero)]
    bar :: [Nat]
    bar = map (either_ pred Succ) [Left Zero, Right (Succ Zero)]
    type family Lambda_0123456789876543210 x where
      Lambda_0123456789876543210 x = Apply (Apply (Apply Either_Sym0 PredSym0) SuccSym0) x
    data Lambda_0123456789876543210Sym0 x0123456789876543210
      where
        Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
                                                       Lambda_0123456789876543210Sym0 x0123456789876543210
    type instance Apply Lambda_0123456789876543210Sym0 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym0KindInference ())
    type family Lambda_0123456789876543210Sym1 x0123456789876543210 where
      Lambda_0123456789876543210Sym1 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210
    type BarSym0 :: [Nat]
    type family BarSym0 :: [Nat] where
      BarSym0 = Bar
    type FooSym0 :: [Nat]
    type family FooSym0 :: [Nat] where
      FooSym0 = Foo
    type Bar :: [Nat]
    type family Bar :: [Nat] where
      Bar = Apply (Apply MapSym0 (Apply (Apply Either_Sym0 PredSym0) SuccSym0)) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
    type Foo :: [Nat]
    type family Foo :: [Nat] where
      Foo = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
    sBar :: (Sing (BarSym0 :: [Nat]) :: Type)
    sFoo :: (Sing (FooSym0 :: [Nat]) :: Type)
    sBar
      = applySing
          (applySing
             (singFun2 @MapSym0 sMap)
             (applySing
                (applySing
                   (singFun3 @Either_Sym0 sEither_) (singFun1 @PredSym0 sPred))
                (singFun1 @SuccSym0 SSucc)))
          (applySing
             (applySing
                (singFun2 @(:@#@$) SCons)
                (applySing (singFun1 @LeftSym0 SLeft) SZero))
             (applySing
                (applySing
                   (singFun2 @(:@#@$) SCons)
                   (applySing
                      (singFun1 @RightSym0 SRight)
                      (applySing (singFun1 @SuccSym0 SSucc) SZero)))
                SNil))
    sFoo
      = applySing
          (applySing
             (singFun2 @MapSym0 sMap)
             (singFun1
                @Lambda_0123456789876543210Sym0
                (\ sX
                   -> case sX of
                        (_ :: Sing x)
                          -> applySing
                               (applySing
                                  (applySing
                                     (singFun3 @Either_Sym0 sEither_) (singFun1 @PredSym0 sPred))
                                  (singFun1 @SuccSym0 SSucc))
                               sX)))
          (applySing
             (applySing
                (singFun2 @(:@#@$) SCons)
                (applySing (singFun1 @LeftSym0 SLeft) SZero))
             (applySing
                (applySing
                   (singFun2 @(:@#@$) SCons)
                   (applySing
                      (singFun1 @RightSym0 SRight)
                      (applySing (singFun1 @SuccSym0 SSucc) SZero)))
                SNil))