Singletons/Sections.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| (+) :: Nat -> Nat -> Nat
          Zero + m = m
          (Succ n) + m = Succ (n + m)
          foo1 :: [Nat]
          foo1 = map ((Succ Zero) +) [Zero, Succ Zero]
          foo2 :: [Nat]
          foo2 = map (+ (Succ Zero)) [Zero, Succ Zero]
          foo3 :: [Nat]
          foo3 = zipWith (+) [Succ Zero, Succ Zero] [Zero, Succ Zero] |]
  ======>
    (+) :: Nat -> Nat -> Nat
    (+) Zero m = m
    (+) (Succ n) m = Succ (n + m)
    foo1 :: [Nat]
    foo1 = (map (Succ Zero +)) [Zero, Succ Zero]
    foo2 :: [Nat]
    foo2 = (map (+ Succ Zero)) [Zero, Succ Zero]
    foo3 :: [Nat]
    foo3 = ((zipWith (+)) [Succ Zero, Succ Zero]) [Zero, Succ Zero]
    type family Lambda_0123456789876543210 t where
      Lambda_0123456789876543210 lhs_0123456789876543210 = Apply (Apply (:+$) lhs_0123456789876543210) (Apply SuccSym0 ZeroSym0)
    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 (:+$$$) (t :: Nat) (t :: Nat) = (:+) t t
    instance SuppressUnusedWarnings (:+$$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:+$$###)) GHC.Tuple.())
    data (:+$$) (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply ((:+$$) l) arg) ((:+$$$) l arg) =>
        (:+$$###)
    type instance Apply ((:+$$) l) l = (:+) l l
    instance SuppressUnusedWarnings (:+$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:+$###)) GHC.Tuple.())
    data (:+$) (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
      = forall arg. SameKind (Apply (:+$) arg) ((:+$$) arg) => (:+$###)
    type instance Apply (:+$) l = (:+$$) l
    type Foo1Sym0 = Foo1
    type Foo2Sym0 = Foo2
    type Foo3Sym0 = Foo3
    type family (:+) (a :: Nat) (a :: Nat) :: Nat where
      (:+) Zero m = m
      (:+) (Succ n) m = Apply SuccSym0 (Apply (Apply (:+$) n) m)
    type family Foo1 :: [Nat] where
      = Apply (Apply MapSym0 (Apply (:+$) (Apply SuccSym0 ZeroSym0))) (Apply (Apply (:$) ZeroSym0) (Apply (Apply (:$) (Apply SuccSym0 ZeroSym0)) '[]))
    type family Foo2 :: [Nat] where
      = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:$) ZeroSym0) (Apply (Apply (:$) (Apply SuccSym0 ZeroSym0)) '[]))
    type family Foo3 :: [Nat] where
      = Apply (Apply (Apply ZipWithSym0 (:+$)) (Apply (Apply (:$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:$) (Apply SuccSym0 ZeroSym0)) '[]))) (Apply (Apply (:$) ZeroSym0) (Apply (Apply (:$) (Apply SuccSym0 ZeroSym0)) '[]))
    (%:+) ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t :: Nat)
    sFoo1 :: Sing (Foo1Sym0 :: [Nat])
    sFoo2 :: Sing (Foo2Sym0 :: [Nat])
    sFoo3 :: Sing (Foo3Sym0 :: [Nat])
    (%:+) SZero (sM :: Sing m) = sM
    (%:+) (SSucc (sN :: Sing n)) (sM :: Sing m)
      = (applySing ((singFun1 @SuccSym0) SSucc))
          ((applySing ((applySing ((singFun2 @(:+$)) (%:+))) sN)) sM)
    sFoo1
      = (applySing
           ((applySing ((singFun2 @MapSym0) sMap))
              ((applySing ((singFun2 @(:+$)) (%:+)))
                 ((applySing ((singFun1 @SuccSym0) SSucc)) SZero))))
          ((applySing ((applySing ((singFun2 @(:$)) SCons)) SZero))
             ((applySing
                 ((applySing ((singFun2 @(:$)) SCons))
                    ((applySing ((singFun1 @SuccSym0) SSucc)) SZero)))
                SNil))
    sFoo2
      = (applySing
           ((applySing ((singFun2 @MapSym0) sMap))
              ((singFun1 @Lambda_0123456789876543210Sym0)
                 (\ sLhs_0123456789876543210
                    -> case sLhs_0123456789876543210 of {
                         _ :: Sing lhs_0123456789876543210
                           -> (applySing
                                 ((applySing ((singFun2 @(:+$)) (%:+))) sLhs_0123456789876543210))
                                ((applySing ((singFun1 @SuccSym0) SSucc)) SZero) }))))
          ((applySing ((applySing ((singFun2 @(:$)) SCons)) SZero))
             ((applySing
                 ((applySing ((singFun2 @(:$)) SCons))
                    ((applySing ((singFun1 @SuccSym0) SSucc)) SZero)))
                SNil))
    sFoo3
      = (applySing
           ((applySing
               ((applySing ((singFun3 @ZipWithSym0) sZipWith))
                  ((singFun2 @(:+$)) (%:+))))
              ((applySing
                  ((applySing ((singFun2 @(:$)) SCons))
                     ((applySing ((singFun1 @SuccSym0) SSucc)) SZero)))
                 ((applySing
                     ((applySing ((singFun2 @(:$)) SCons))
                        ((applySing ((singFun1 @SuccSym0) SSucc)) SZero)))
                    SNil))))
          ((applySing ((applySing ((singFun2 @(:$)) SCons)) SZero))
             ((applySing
                 ((applySing ((singFun2 @(:$)) SCons))
                    ((applySing ((singFun1 @SuccSym0) SSucc)) SZero)))
                SNil))