packages feed

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))