packages feed

singletons-1.0: tests/compile-and-dump/Singletons/LambdasComprehensive.ghc78.template

Singletons/LambdasComprehensive.hs: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)] |]
  ======>
    Singletons/LambdasComprehensive.hs:(0,0)-(0,0)
    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. (GHC.Types.~) (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 Bar =
        (Apply (Apply MapSym0 (Apply (Apply Either_Sym0 PredSym0) SuccSym0)) (Apply (Apply (:$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) GHC.Types.[])) :: GHC.Types.[] Nat)
    type Foo =
        (Apply (Apply MapSym0 Lambda_0123456789Sym0) (Apply (Apply (:$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) GHC.Types.[])) :: GHC.Types.[] Nat)
    sBar :: Sing BarSym0
    sFoo :: Sing FooSym0
    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))