singletons-2.5: tests/compile-and-dump/Singletons/LambdasComprehensive.ghc86.template
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))