singletons-2.1: tests/compile-and-dump/Singletons/LambdasComprehensive.ghc80.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_0123456789 t where
Lambda_0123456789 x = Apply (Apply (Apply Either_Sym0 PredSym0) SuccSym0) x
type Lambda_0123456789Sym1 t = Lambda_0123456789 t
instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
data Lambda_0123456789Sym0 l
= forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
Lambda_0123456789Sym0KindInference
type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
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_0123456789Sym0) (Apply (Apply (:$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) '[]))
sBar :: Sing (BarSym0 :: [Nat])
sFoo :: Sing (FooSym0 :: [Nat])
sBar
= applySing
(applySing
(singFun2 (Proxy :: Proxy MapSym0) sMap)
(applySing
(applySing
(singFun3 (Proxy :: Proxy Either_Sym0) sEither_)
(singFun1 (Proxy :: Proxy PredSym0) sPred))
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing (singFun1 (Proxy :: Proxy LeftSym0) SLeft) SZero))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing
(singFun1 (Proxy :: Proxy RightSym0) SRight)
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero)))
SNil))
sFoo
= applySing
(applySing
(singFun2 (Proxy :: Proxy MapSym0) sMap)
(singFun1
(Proxy :: Proxy Lambda_0123456789Sym0)
(\ sX
-> let
lambda :: forall x. Sing x -> Sing (Apply Lambda_0123456789Sym0 x)
lambda x
= applySing
(applySing
(applySing
(singFun3 (Proxy :: Proxy Either_Sym0) sEither_)
(singFun1 (Proxy :: Proxy PredSym0) sPred))
(singFun1 (Proxy :: Proxy SuccSym0) SSucc))
x
in lambda sX)))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing (singFun1 (Proxy :: Proxy LeftSym0) SLeft) SZero))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing
(singFun1 (Proxy :: Proxy RightSym0) SRight)
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero)))
SNil))