LambdasComprehensive.golden

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 LamCases_0123456789876543210 a_0123456789876543210 where
      LamCases_0123456789876543210 x = Apply (Apply (Apply Either_Sym0 PredSym0) SuccSym0) x
    data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
      where
        LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
                                                         LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
    type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) LamCases_0123456789876543210Sym0KindInference ())
    type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
      LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
    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 LamCases_0123456789876543210Sym0) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
    sBar :: (Sing (Bar :: [Nat]) :: Type)
    sFoo :: (Sing (Foo :: [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
                @LamCases_0123456789876543210Sym0
                (\cases
                   (sX :: 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))