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 t where Lambda_0123456789876543210 x = Apply (Apply (Apply Either_Sym0 PredSym0) SuccSym0) x type Lambda_0123456789876543210Sym1 t0123456789876543210 = Lambda_0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Lambda_0123456789876543210Sym0KindInference) ()) data Lambda_0123456789876543210Sym0 t0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) => Lambda_0123456789876543210Sym0 t0123456789876543210 type instance Apply Lambda_0123456789876543210Sym0 t0123456789876543210 = Lambda_0123456789876543210 t0123456789876543210 type BarSym0 = Bar type FooSym0 = Foo 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))) '[])) type family Foo :: [Nat] where Foo = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) '[])) sBar :: Sing (BarSym0 :: [Nat]) sFoo :: Sing (FooSym0 :: [Nat]) 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))