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]) :: Type)
    sFoo2 :: (Sing (Foo2Sym0 :: [Nat]) :: Type)
    sFoo1 :: (Sing (Foo1Sym0 :: [Nat]) :: Type)
    (%+) ::
      (forall (t :: Nat) (t :: Nat).
       Sing t
       -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: Nat) :: Type)
    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)