packages feed

singletons-2.4: tests/compile-and-dump/Singletons/LambdasComprehensive.ghc84.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 t =
        Lambda_0123456789876543210 t
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Lambda_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Lambda_0123456789876543210Sym0 l
      = forall arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
        Lambda_0123456789876543210Sym0KindInference
    type instance Apply Lambda_0123456789876543210Sym0 l = Lambda_0123456789876543210 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_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))