Sections.ghc76.template

Promote/Sections.hs:0:0: Splicing declarations
    promote
      [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] |]
  ======>
    Promote/Sections.hs:(0,0)-(0,0)
    + :: 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 Foo1 =
        Apply (Apply MapSym0 (Apply :+$ (Apply SuccSym0 ZeroSym0))) '[ZeroSym0,
                                                                      Apply SuccSym0 ZeroSym0]
    type Foo1Sym0 = Foo1
    type Foo2 =
        Apply (Apply MapSym0 Lambda_0123456789Sym0) '[ZeroSym0,
                                                      Apply SuccSym0 ZeroSym0]
    type Foo2Sym0 = Foo2
    type family Lambda_0123456789 (t :: k) :: r
    type instance Lambda_0123456789 x =
        Apply (Apply :+$ x) (Apply SuccSym0 ZeroSym0)
    data Lambda_0123456789Sym0 (k :: TyFun k r)
    type instance Apply Lambda_0123456789Sym0 a = Lambda_0123456789 a
    type Foo3 =
        Apply (Apply (Apply ZipWithSym0 :+$) '[Apply SuccSym0 ZeroSym0,
                                               Apply SuccSym0 ZeroSym0]) '[ZeroSym0,
                                                                           Apply SuccSym0 ZeroSym0]
    type Foo3Sym0 = Foo3
    type family (:+) (a :: Nat) (a :: Nat) :: Nat
    type instance (:+) Zero m = m
    type instance (:+) (Succ n) m =
        Apply SuccSym0 (Apply (Apply :+$ n) m)
    data (:+$$) (l :: Nat) (l :: TyFun Nat Nat)
    data (:+$) (k :: TyFun Nat (TyFun Nat Nat -> *))
    type instance Apply (:+$$ a) a = :+ a a
    type instance Apply :+$ a = :+$$ a