singletons-base-3.3: tests/compile-and-dump/Singletons/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 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))