Sections.golden

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 lhs_0123456789876543210 where
      Lambda_0123456789876543210 lhs_0123456789876543210 = Apply (Apply (+@#@$) lhs_0123456789876543210) (Apply SuccSym0 ZeroSym0)
    data Lambda_0123456789876543210Sym0 lhs_01234567898765432100123456789876543210
      where
        Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
                                                       Lambda_0123456789876543210Sym0 lhs_01234567898765432100123456789876543210
    type instance Apply Lambda_0123456789876543210Sym0 lhs_01234567898765432100123456789876543210 = Lambda_0123456789876543210 lhs_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
    type family Lambda_0123456789876543210Sym1 lhs_01234567898765432100123456789876543210 where
      Lambda_0123456789876543210Sym1 lhs_01234567898765432100123456789876543210 = Lambda_0123456789876543210 lhs_01234567898765432100123456789876543210
    type Foo3Sym0 :: [Nat]
    type family Foo3Sym0 :: [Nat] where
      Foo3Sym0 = Foo3
    type Foo2Sym0 :: [Nat]
    type family Foo2Sym0 :: [Nat] where
      Foo2Sym0 = Foo2
    type Foo1Sym0 :: [Nat]
    type family Foo1Sym0 :: [Nat] where
      Foo1Sym0 = Foo1
    type (+@#@$) :: (~>) Nat ((~>) Nat Nat)
    data (+@#@$) :: (~>) Nat ((~>) Nat Nat)
      where
        (:+@#@$###) :: SameKind (Apply (+@#@$) arg) ((+@#@$$) arg) =>
                       (+@#@$) a0123456789876543210
    type instance Apply (+@#@$) a0123456789876543210 = (+@#@$$) a0123456789876543210
    instance SuppressUnusedWarnings (+@#@$) where
      suppressUnusedWarnings = snd (((,) (:+@#@$###)) ())
    type (+@#@$$) :: Nat -> (~>) Nat Nat
    data (+@#@$$) (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        (:+@#@$$###) :: SameKind (Apply ((+@#@$$) a0123456789876543210) arg) ((+@#@$$$) a0123456789876543210 arg) =>
                        (+@#@$$) a0123456789876543210 a0123456789876543210
    type instance Apply ((+@#@$$) a0123456789876543210) a0123456789876543210 = (+) a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((+@#@$$) a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) (:+@#@$$###)) ())
    type (+@#@$$$) :: Nat -> Nat -> Nat
    type family (+@#@$$$) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      (+@#@$$$) a0123456789876543210 a0123456789876543210 = (+) a0123456789876543210 a0123456789876543210
    type Foo3 :: [Nat]
    type family Foo3 :: [Nat] where
      Foo3 = Apply (Apply (Apply ZipWithSym0 (+@#@$)) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) NilSym0))) (Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) NilSym0))
    type Foo2 :: [Nat]
    type family Foo2 :: [Nat] where
      Foo2 = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) NilSym0))
    type Foo1 :: [Nat]
    type family Foo1 :: [Nat] where
      Foo1 = Apply (Apply MapSym0 (Apply (+@#@$) (Apply SuccSym0 ZeroSym0))) (Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) NilSym0))
    type (+) :: Nat -> Nat -> Nat
    type family (+) (a :: Nat) (a :: Nat) :: Nat where
      (+) 'Zero m = m
      (+) ('Succ n) m = Apply SuccSym0 (Apply (Apply (+@#@$) n) m)
    sFoo3 :: Sing (Foo3Sym0 :: [Nat])
    sFoo2 :: Sing (Foo2Sym0 :: [Nat])
    sFoo1 :: Sing (Foo1Sym0 :: [Nat])
    (%+) ::
      forall (t :: Nat) (t :: Nat). Sing t
                                    -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: Nat)
    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))
    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))
    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))
    (%+) SZero (sM :: Sing m) = sM
    (%+) (SSucc (sN :: Sing n)) (sM :: Sing m)
      = (applySing ((singFun1 @SuccSym0) SSucc))
          ((applySing ((applySing ((singFun2 @(+@#@$)) (%+))) sN)) sM)
    instance SingI ((+@#@$) :: (~>) Nat ((~>) Nat Nat)) where
      sing = (singFun2 @(+@#@$)) (%+)
    instance SingI d =>
             SingI ((+@#@$$) (d :: Nat) :: (~>) Nat Nat) where
      sing = (singFun1 @((+@#@$$) (d :: Nat))) ((%+) (sing @d))
    instance SingI1 ((+@#@$$) :: Nat -> (~>) Nat Nat) where
      liftSing (s :: Sing (d :: Nat))
        = (singFun1 @((+@#@$$) (d :: Nat))) ((%+) s)