packages feed

singletons-base-3.2: tests/compile-and-dump/Singletons/LetStatements.golden

Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| foo1 :: Nat -> Nat
          foo1 x
            = let
                y :: Nat
                y = Succ Zero
              in y
          foo2 :: Nat
          foo2
            = let
                y = Succ Zero
                z = Succ y
              in z
          foo3 :: Nat -> Nat
          foo3 x
            = let
                y :: Nat
                y = Succ x
              in y
          foo4 :: Nat -> Nat
          foo4 x
            = let
                f :: Nat -> Nat
                f y = Succ y
              in f x
          foo5 :: Nat -> Nat
          foo5 x
            = let
                f :: Nat -> Nat
                f y
                  = let
                      z :: Nat
                      z = Succ y
                    in Succ z
              in f x
          foo6 :: Nat -> Nat
          foo6 x
            = let
                f :: Nat -> Nat
                f y = Succ y in
              let
                z :: Nat
                z = f x
              in z
          foo7 :: Nat -> Nat
          foo7 x
            = let
                x :: Nat
                x = Zero
              in x
          foo8 :: Nat -> Nat
          foo8 x
            = let
                z :: Nat
                z = (\ x -> x) Zero
              in z
          foo9 :: Nat -> Nat
          foo9 x
            = let
                z :: Nat -> Nat
                z = (\ x -> x)
              in z x
          foo10 :: Nat -> Nat
          foo10 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + m)
              in (Succ Zero) + x
          foo11 :: Nat -> Nat
          foo11 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + m)
                z :: Nat
                z = x
              in (Succ Zero) + z
          foo12 :: Nat -> Nat
          foo12 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + x)
              in x + (Succ (Succ Zero))
          foo13 :: forall a. a -> a
          foo13 x
            = let
                bar :: a
                bar = x
              in foo13_ bar
          foo13_ :: a -> a
          foo13_ y = y
          foo14 :: Nat -> (Nat, Nat)
          foo14 x = let (y, z) = (Succ x, x) in (z, y) |]
  ======>
    foo1 :: Nat -> Nat
    foo1 x
      = let
          y :: Nat
          y = Succ Zero
        in y
    foo2 :: Nat
    foo2
      = let
          y = Succ Zero
          z = Succ y
        in z
    foo3 :: Nat -> Nat
    foo3 x
      = let
          y :: Nat
          y = Succ x
        in y
    foo4 :: Nat -> Nat
    foo4 x
      = let
          f :: Nat -> Nat
          f y = Succ y
        in f x
    foo5 :: Nat -> Nat
    foo5 x
      = let
          f :: Nat -> Nat
          f y
            = let
                z :: Nat
                z = Succ y
              in Succ z
        in f x
    foo6 :: Nat -> Nat
    foo6 x
      = let
          f :: Nat -> Nat
          f y = Succ y in
        let
          z :: Nat
          z = f x
        in z
    foo7 :: Nat -> Nat
    foo7 x
      = let
          x :: Nat
          x = Zero
        in x
    foo8 :: Nat -> Nat
    foo8 x
      = let
          z :: Nat
          z = (\ x -> x) Zero
        in z
    foo9 :: Nat -> Nat
    foo9 x
      = let
          z :: Nat -> Nat
          z = \ x -> x
        in z x
    foo10 :: Nat -> Nat
    foo10 x
      = let
          (+) :: Nat -> Nat -> Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + m)
        in (Succ Zero + x)
    foo11 :: Nat -> Nat
    foo11 x
      = let
          (+) :: Nat -> Nat -> Nat
          z :: Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + m)
          z = x
        in (Succ Zero + z)
    foo12 :: Nat -> Nat
    foo12 x
      = let
          (+) :: Nat -> Nat -> Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + x)
        in (x + Succ (Succ Zero))
    foo13 :: forall a. a -> a
    foo13 x
      = let
          bar :: a
          bar = x
        in foo13_ bar
    foo13_ :: a -> a
    foo13_ y = y
    foo14 :: Nat -> (Nat, Nat)
    foo14 x = let (y, z) = (Succ x, x) in (z, y)
    type family Case_0123456789876543210 x t where
      Case_0123456789876543210 x '(_,
                                   y_0123456789876543210) = y_0123456789876543210
    type family Case_0123456789876543210 x t where
      Case_0123456789876543210 x '(y_0123456789876543210,
                                   _) = y_0123456789876543210
    data Let0123456789876543210ZSym0 x0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 x0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    type family Let0123456789876543210ZSym1 x0123456789876543210 where
      Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    data Let0123456789876543210YSym0 x0123456789876543210
      where
        Let0123456789876543210YSym0KindInference :: SameKind (Apply Let0123456789876543210YSym0 arg) (Let0123456789876543210YSym1 arg) =>
                                                    Let0123456789876543210YSym0 x0123456789876543210
    type instance Apply Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210YSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210YSym0KindInference ())
    type family Let0123456789876543210YSym1 x0123456789876543210 where
      Let0123456789876543210YSym1 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    data Let0123456789876543210X_0123456789876543210Sym0 x0123456789876543210
      where
        Let0123456789876543210X_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210X_0123456789876543210Sym0 arg) (Let0123456789876543210X_0123456789876543210Sym1 arg) =>
                                                                        Let0123456789876543210X_0123456789876543210Sym0 x0123456789876543210
    type instance Apply Let0123456789876543210X_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210X_0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210X_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((,)
               Let0123456789876543210X_0123456789876543210Sym0KindInference ())
    type family Let0123456789876543210X_0123456789876543210Sym1 x0123456789876543210 where
      Let0123456789876543210X_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210X_0123456789876543210 x0123456789876543210
    type family Let0123456789876543210Z x where
      Let0123456789876543210Z x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)
    type family Let0123456789876543210Y x where
      Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)
    type family Let0123456789876543210X_0123456789876543210 x where
      Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x
    data Let0123456789876543210BarSym0 x0123456789876543210
      where
        Let0123456789876543210BarSym0KindInference :: SameKind (Apply Let0123456789876543210BarSym0 arg) (Let0123456789876543210BarSym1 arg) =>
                                                      Let0123456789876543210BarSym0 x0123456789876543210
    type instance Apply Let0123456789876543210BarSym0 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210BarSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210BarSym0KindInference ())
    type family Let0123456789876543210BarSym1 x0123456789876543210 :: a0123456789876543210 where
      Let0123456789876543210BarSym1 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
    type family Let0123456789876543210Bar x :: a where
      Let0123456789876543210Bar x = x
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) =>
                                             (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
    type instance Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210
    instance SuppressUnusedWarnings (<<<%%%%%%%%%%%%%%%%%%%%@#@$) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat)
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 arg) =>
                                              (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 arg) =>
                                               (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ())
    type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m
      (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) n) x)
    data Let0123456789876543210ZSym0 x0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 x0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    type family Let0123456789876543210ZSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) =>
                                             (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
    type instance Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210
    instance SuppressUnusedWarnings (<<<%%%%%%%%%%%%%%%%%%%%@#@$) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat)
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 arg) =>
                                              (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 arg) =>
                                               (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ())
    type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type family Let0123456789876543210Z x :: Nat where
      Let0123456789876543210Z x = x
    type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m
      (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) n) m)
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) =>
                                             (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
    type instance Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210
    instance SuppressUnusedWarnings (<<<%%%%%%%%%%%%%%%%%%%%@#@$) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat)
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 arg) =>
                                              (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ())
    data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 arg) =>
                                               (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ())
    type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210
    type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where
      (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m
      (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) n) m)
    type family Lambda_0123456789876543210 a_0123456789876543210 x x where
      Lambda_0123456789876543210 a_0123456789876543210 x x = x
    data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
      where
        Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
                                                       Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
    type instance Apply Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym0KindInference ())
    data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210
      where
        Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) x0123456789876543210 = Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym1KindInference ())
    data Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210
      where
        Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 x0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym2KindInference ())
    type family Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 where
      Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210
    data Let0123456789876543210ZSym0 x0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 x0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210ZSym1 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    data Let0123456789876543210ZSym1 x0123456789876543210 :: (~>) Nat Nat
      where
        Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 x0123456789876543210) arg) (Let0123456789876543210ZSym2 x0123456789876543210 arg) =>
                                                    Let0123456789876543210ZSym1 x0123456789876543210 a0123456789876543210
    type instance Apply (Let0123456789876543210ZSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210Z x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym1KindInference ())
    type family Let0123456789876543210ZSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where
      Let0123456789876543210ZSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210Z x0123456789876543210 a0123456789876543210
    type family Let0123456789876543210Z x (a :: Nat) :: Nat where
      Let0123456789876543210Z x a_0123456789876543210 = Apply (Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) x) a_0123456789876543210
    type family Lambda_0123456789876543210 x x where
      Lambda_0123456789876543210 x x = x
    data Lambda_0123456789876543210Sym0 x0123456789876543210
      where
        Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
                                                       Lambda_0123456789876543210Sym0 x0123456789876543210
    type instance Apply Lambda_0123456789876543210Sym0 x0123456789876543210 = Lambda_0123456789876543210Sym1 x0123456789876543210
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym0KindInference ())
    data Lambda_0123456789876543210Sym1 x0123456789876543210 x0123456789876543210
      where
        Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym1 x0123456789876543210 x0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym1KindInference ())
    type family Lambda_0123456789876543210Sym2 x0123456789876543210 x0123456789876543210 where
      Lambda_0123456789876543210Sym2 x0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 x0123456789876543210
    data Let0123456789876543210ZSym0 x0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 x0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    type family Let0123456789876543210ZSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    type family Let0123456789876543210Z x :: Nat where
      Let0123456789876543210Z x = Apply (Apply Lambda_0123456789876543210Sym0 x) ZeroSym0
    data Let0123456789876543210XSym0 x0123456789876543210
      where
        Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) =>
                                                    Let0123456789876543210XSym0 x0123456789876543210
    type instance Apply Let0123456789876543210XSym0 x0123456789876543210 = Let0123456789876543210X x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210XSym0KindInference ())
    type family Let0123456789876543210XSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210XSym1 x0123456789876543210 = Let0123456789876543210X x0123456789876543210
    type family Let0123456789876543210X x :: Nat where
      Let0123456789876543210X x = ZeroSym0
    data Let0123456789876543210FSym0 x0123456789876543210
      where
        Let0123456789876543210FSym0KindInference :: SameKind (Apply Let0123456789876543210FSym0 arg) (Let0123456789876543210FSym1 arg) =>
                                                    Let0123456789876543210FSym0 x0123456789876543210
    type instance Apply Let0123456789876543210FSym0 x0123456789876543210 = Let0123456789876543210FSym1 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210FSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym0KindInference ())
    data Let0123456789876543210FSym1 x0123456789876543210 :: (~>) Nat Nat
      where
        Let0123456789876543210FSym1KindInference :: SameKind (Apply (Let0123456789876543210FSym1 x0123456789876543210) arg) (Let0123456789876543210FSym2 x0123456789876543210 arg) =>
                                                    Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210
    type instance Apply (Let0123456789876543210FSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210FSym1 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym1KindInference ())
    type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where
      Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    type family Let0123456789876543210F x (a :: Nat) :: Nat where
      Let0123456789876543210F x y = Apply SuccSym0 y
    data Let0123456789876543210ZSym0 x0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 x0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    type family Let0123456789876543210ZSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210
    type family Let0123456789876543210Z x :: Nat where
      Let0123456789876543210Z x = Apply (Let0123456789876543210FSym1 x) x
    data Let0123456789876543210ZSym0 y0123456789876543210
      where
        Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
                                                    Let0123456789876543210ZSym0 y0123456789876543210
    type instance Apply Let0123456789876543210ZSym0 y0123456789876543210 = Let0123456789876543210ZSym1 y0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym0KindInference ())
    data Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
      where
        Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 y0123456789876543210) arg) (Let0123456789876543210ZSym2 y0123456789876543210 arg) =>
                                                    Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
    type instance Apply (Let0123456789876543210ZSym1 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 y0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210ZSym1KindInference ())
    type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: Nat where
      Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
    type family Let0123456789876543210Z y x :: Nat where
      Let0123456789876543210Z y x = Apply SuccSym0 y
    data Let0123456789876543210FSym0 x0123456789876543210
      where
        Let0123456789876543210FSym0KindInference :: SameKind (Apply Let0123456789876543210FSym0 arg) (Let0123456789876543210FSym1 arg) =>
                                                    Let0123456789876543210FSym0 x0123456789876543210
    type instance Apply Let0123456789876543210FSym0 x0123456789876543210 = Let0123456789876543210FSym1 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210FSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym0KindInference ())
    data Let0123456789876543210FSym1 x0123456789876543210 :: (~>) Nat Nat
      where
        Let0123456789876543210FSym1KindInference :: SameKind (Apply (Let0123456789876543210FSym1 x0123456789876543210) arg) (Let0123456789876543210FSym2 x0123456789876543210 arg) =>
                                                    Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210
    type instance Apply (Let0123456789876543210FSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210FSym1 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym1KindInference ())
    type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where
      Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    type family Let0123456789876543210F x (a :: Nat) :: Nat where
      Let0123456789876543210F x y = Apply SuccSym0 (Let0123456789876543210ZSym2 y x)
    data Let0123456789876543210FSym0 x0123456789876543210
      where
        Let0123456789876543210FSym0KindInference :: SameKind (Apply Let0123456789876543210FSym0 arg) (Let0123456789876543210FSym1 arg) =>
                                                    Let0123456789876543210FSym0 x0123456789876543210
    type instance Apply Let0123456789876543210FSym0 x0123456789876543210 = Let0123456789876543210FSym1 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210FSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym0KindInference ())
    data Let0123456789876543210FSym1 x0123456789876543210 :: (~>) Nat Nat
      where
        Let0123456789876543210FSym1KindInference :: SameKind (Apply (Let0123456789876543210FSym1 x0123456789876543210) arg) (Let0123456789876543210FSym2 x0123456789876543210 arg) =>
                                                    Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210
    type instance Apply (Let0123456789876543210FSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210FSym1 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210FSym1KindInference ())
    type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where
      Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210
    type family Let0123456789876543210F x (a :: Nat) :: Nat where
      Let0123456789876543210F x y = Apply SuccSym0 y
    data Let0123456789876543210YSym0 x0123456789876543210
      where
        Let0123456789876543210YSym0KindInference :: SameKind (Apply Let0123456789876543210YSym0 arg) (Let0123456789876543210YSym1 arg) =>
                                                    Let0123456789876543210YSym0 x0123456789876543210
    type instance Apply Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210YSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210YSym0KindInference ())
    type family Let0123456789876543210YSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210YSym1 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    type family Let0123456789876543210Y x :: Nat where
      Let0123456789876543210Y x = Apply SuccSym0 x
    type family Let0123456789876543210ZSym0 where
      Let0123456789876543210ZSym0 = Let0123456789876543210Z
    type family Let0123456789876543210YSym0 where
      Let0123456789876543210YSym0 = Let0123456789876543210Y
    type family Let0123456789876543210Z where
      Let0123456789876543210Z = Apply SuccSym0 Let0123456789876543210YSym0
    type family Let0123456789876543210Y where
      Let0123456789876543210Y = Apply SuccSym0 ZeroSym0
    data Let0123456789876543210YSym0 x0123456789876543210
      where
        Let0123456789876543210YSym0KindInference :: SameKind (Apply Let0123456789876543210YSym0 arg) (Let0123456789876543210YSym1 arg) =>
                                                    Let0123456789876543210YSym0 x0123456789876543210
    type instance Apply Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210YSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210YSym0KindInference ())
    type family Let0123456789876543210YSym1 x0123456789876543210 :: Nat where
      Let0123456789876543210YSym1 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210
    type family Let0123456789876543210Y x :: Nat where
      Let0123456789876543210Y x = Apply SuccSym0 ZeroSym0
    type Foo14Sym0 :: (~>) Nat (Nat, Nat)
    data Foo14Sym0 :: (~>) Nat (Nat, Nat)
      where
        Foo14Sym0KindInference :: SameKind (Apply Foo14Sym0 arg) (Foo14Sym1 arg) =>
                                  Foo14Sym0 a0123456789876543210
    type instance Apply Foo14Sym0 a0123456789876543210 = Foo14 a0123456789876543210
    instance SuppressUnusedWarnings Foo14Sym0 where
      suppressUnusedWarnings = snd ((,) Foo14Sym0KindInference ())
    type Foo14Sym1 :: Nat -> (Nat, Nat)
    type family Foo14Sym1 (a0123456789876543210 :: Nat) :: (Nat,
                                                            Nat) where
      Foo14Sym1 a0123456789876543210 = Foo14 a0123456789876543210
    type Foo13_Sym0 :: (~>) a a
    data Foo13_Sym0 :: (~>) a a
      where
        Foo13_Sym0KindInference :: SameKind (Apply Foo13_Sym0 arg) (Foo13_Sym1 arg) =>
                                   Foo13_Sym0 a0123456789876543210
    type instance Apply Foo13_Sym0 a0123456789876543210 = Foo13_ a0123456789876543210
    instance SuppressUnusedWarnings Foo13_Sym0 where
      suppressUnusedWarnings = snd ((,) Foo13_Sym0KindInference ())
    type Foo13_Sym1 :: a -> a
    type family Foo13_Sym1 (a0123456789876543210 :: a) :: a where
      Foo13_Sym1 a0123456789876543210 = Foo13_ a0123456789876543210
    type Foo13Sym0 :: forall a. (~>) a a
    data Foo13Sym0 :: (~>) a a
      where
        Foo13Sym0KindInference :: SameKind (Apply Foo13Sym0 arg) (Foo13Sym1 arg) =>
                                  Foo13Sym0 a0123456789876543210
    type instance Apply Foo13Sym0 a0123456789876543210 = Foo13 a0123456789876543210
    instance SuppressUnusedWarnings Foo13Sym0 where
      suppressUnusedWarnings = snd ((,) Foo13Sym0KindInference ())
    type Foo13Sym1 :: forall a. a -> a
    type family Foo13Sym1 (a0123456789876543210 :: a) :: a where
      Foo13Sym1 a0123456789876543210 = Foo13 a0123456789876543210
    type Foo12Sym0 :: (~>) Nat Nat
    data Foo12Sym0 :: (~>) Nat Nat
      where
        Foo12Sym0KindInference :: SameKind (Apply Foo12Sym0 arg) (Foo12Sym1 arg) =>
                                  Foo12Sym0 a0123456789876543210
    type instance Apply Foo12Sym0 a0123456789876543210 = Foo12 a0123456789876543210
    instance SuppressUnusedWarnings Foo12Sym0 where
      suppressUnusedWarnings = snd ((,) Foo12Sym0KindInference ())
    type Foo12Sym1 :: Nat -> Nat
    type family Foo12Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo12Sym1 a0123456789876543210 = Foo12 a0123456789876543210
    type Foo11Sym0 :: (~>) Nat Nat
    data Foo11Sym0 :: (~>) Nat Nat
      where
        Foo11Sym0KindInference :: SameKind (Apply Foo11Sym0 arg) (Foo11Sym1 arg) =>
                                  Foo11Sym0 a0123456789876543210
    type instance Apply Foo11Sym0 a0123456789876543210 = Foo11 a0123456789876543210
    instance SuppressUnusedWarnings Foo11Sym0 where
      suppressUnusedWarnings = snd ((,) Foo11Sym0KindInference ())
    type Foo11Sym1 :: Nat -> Nat
    type family Foo11Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo11Sym1 a0123456789876543210 = Foo11 a0123456789876543210
    type Foo10Sym0 :: (~>) Nat Nat
    data Foo10Sym0 :: (~>) Nat Nat
      where
        Foo10Sym0KindInference :: SameKind (Apply Foo10Sym0 arg) (Foo10Sym1 arg) =>
                                  Foo10Sym0 a0123456789876543210
    type instance Apply Foo10Sym0 a0123456789876543210 = Foo10 a0123456789876543210
    instance SuppressUnusedWarnings Foo10Sym0 where
      suppressUnusedWarnings = snd ((,) Foo10Sym0KindInference ())
    type Foo10Sym1 :: Nat -> Nat
    type family Foo10Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo10Sym1 a0123456789876543210 = Foo10 a0123456789876543210
    type Foo9Sym0 :: (~>) Nat Nat
    data Foo9Sym0 :: (~>) Nat Nat
      where
        Foo9Sym0KindInference :: SameKind (Apply Foo9Sym0 arg) (Foo9Sym1 arg) =>
                                 Foo9Sym0 a0123456789876543210
    type instance Apply Foo9Sym0 a0123456789876543210 = Foo9 a0123456789876543210
    instance SuppressUnusedWarnings Foo9Sym0 where
      suppressUnusedWarnings = snd ((,) Foo9Sym0KindInference ())
    type Foo9Sym1 :: Nat -> Nat
    type family Foo9Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo9Sym1 a0123456789876543210 = Foo9 a0123456789876543210
    type Foo8Sym0 :: (~>) Nat Nat
    data Foo8Sym0 :: (~>) Nat Nat
      where
        Foo8Sym0KindInference :: SameKind (Apply Foo8Sym0 arg) (Foo8Sym1 arg) =>
                                 Foo8Sym0 a0123456789876543210
    type instance Apply Foo8Sym0 a0123456789876543210 = Foo8 a0123456789876543210
    instance SuppressUnusedWarnings Foo8Sym0 where
      suppressUnusedWarnings = snd ((,) Foo8Sym0KindInference ())
    type Foo8Sym1 :: Nat -> Nat
    type family Foo8Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo8Sym1 a0123456789876543210 = Foo8 a0123456789876543210
    type Foo7Sym0 :: (~>) Nat Nat
    data Foo7Sym0 :: (~>) Nat Nat
      where
        Foo7Sym0KindInference :: SameKind (Apply Foo7Sym0 arg) (Foo7Sym1 arg) =>
                                 Foo7Sym0 a0123456789876543210
    type instance Apply Foo7Sym0 a0123456789876543210 = Foo7 a0123456789876543210
    instance SuppressUnusedWarnings Foo7Sym0 where
      suppressUnusedWarnings = snd ((,) Foo7Sym0KindInference ())
    type Foo7Sym1 :: Nat -> Nat
    type family Foo7Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo7Sym1 a0123456789876543210 = Foo7 a0123456789876543210
    type Foo6Sym0 :: (~>) Nat Nat
    data Foo6Sym0 :: (~>) Nat Nat
      where
        Foo6Sym0KindInference :: SameKind (Apply Foo6Sym0 arg) (Foo6Sym1 arg) =>
                                 Foo6Sym0 a0123456789876543210
    type instance Apply Foo6Sym0 a0123456789876543210 = Foo6 a0123456789876543210
    instance SuppressUnusedWarnings Foo6Sym0 where
      suppressUnusedWarnings = snd ((,) Foo6Sym0KindInference ())
    type Foo6Sym1 :: Nat -> Nat
    type family Foo6Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo6Sym1 a0123456789876543210 = Foo6 a0123456789876543210
    type Foo5Sym0 :: (~>) Nat Nat
    data Foo5Sym0 :: (~>) Nat Nat
      where
        Foo5Sym0KindInference :: SameKind (Apply Foo5Sym0 arg) (Foo5Sym1 arg) =>
                                 Foo5Sym0 a0123456789876543210
    type instance Apply Foo5Sym0 a0123456789876543210 = Foo5 a0123456789876543210
    instance SuppressUnusedWarnings Foo5Sym0 where
      suppressUnusedWarnings = snd ((,) Foo5Sym0KindInference ())
    type Foo5Sym1 :: Nat -> Nat
    type family Foo5Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo5Sym1 a0123456789876543210 = Foo5 a0123456789876543210
    type Foo4Sym0 :: (~>) Nat Nat
    data Foo4Sym0 :: (~>) Nat Nat
      where
        Foo4Sym0KindInference :: SameKind (Apply Foo4Sym0 arg) (Foo4Sym1 arg) =>
                                 Foo4Sym0 a0123456789876543210
    type instance Apply Foo4Sym0 a0123456789876543210 = Foo4 a0123456789876543210
    instance SuppressUnusedWarnings Foo4Sym0 where
      suppressUnusedWarnings = snd ((,) Foo4Sym0KindInference ())
    type Foo4Sym1 :: Nat -> Nat
    type family Foo4Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo4Sym1 a0123456789876543210 = Foo4 a0123456789876543210
    type Foo3Sym0 :: (~>) Nat Nat
    data Foo3Sym0 :: (~>) Nat Nat
      where
        Foo3Sym0KindInference :: SameKind (Apply Foo3Sym0 arg) (Foo3Sym1 arg) =>
                                 Foo3Sym0 a0123456789876543210
    type instance Apply Foo3Sym0 a0123456789876543210 = Foo3 a0123456789876543210
    instance SuppressUnusedWarnings Foo3Sym0 where
      suppressUnusedWarnings = snd ((,) Foo3Sym0KindInference ())
    type Foo3Sym1 :: Nat -> Nat
    type family Foo3Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210
    type Foo2Sym0 :: Nat
    type family Foo2Sym0 :: Nat where
      Foo2Sym0 = Foo2
    type Foo1Sym0 :: (~>) Nat Nat
    data Foo1Sym0 :: (~>) Nat Nat
      where
        Foo1Sym0KindInference :: SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
                                 Foo1Sym0 a0123456789876543210
    type instance Apply Foo1Sym0 a0123456789876543210 = Foo1 a0123456789876543210
    instance SuppressUnusedWarnings Foo1Sym0 where
      suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ())
    type Foo1Sym1 :: Nat -> Nat
    type family Foo1Sym1 (a0123456789876543210 :: Nat) :: Nat where
      Foo1Sym1 a0123456789876543210 = Foo1 a0123456789876543210
    type Foo14 :: Nat -> (Nat, Nat)
    type family Foo14 (a :: Nat) :: (Nat, Nat) where
      Foo14 x = Apply (Apply Tuple2Sym0 (Let0123456789876543210ZSym1 x)) (Let0123456789876543210YSym1 x)
    type Foo13_ :: a -> a
    type family Foo13_ (a :: a) :: a where
      Foo13_ y = y
    type Foo13 :: forall a. a -> a
    type family Foo13 (a :: a) :: a where
      Foo13 x = Apply Foo13_Sym0 (Let0123456789876543210BarSym1 x)
    type Foo12 :: Nat -> Nat
    type family Foo12 (a :: Nat) :: Nat where
      Foo12 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))
    type Foo11 :: Nat -> Nat
    type family Foo11 (a :: Nat) :: Nat where
      Foo11 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (Apply SuccSym0 ZeroSym0)) (Let0123456789876543210ZSym1 x)
    type Foo10 :: Nat -> Nat
    type family Foo10 (a :: Nat) :: Nat where
      Foo10 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (Apply SuccSym0 ZeroSym0)) x
    type Foo9 :: Nat -> Nat
    type family Foo9 (a :: Nat) :: Nat where
      Foo9 x = Apply (Let0123456789876543210ZSym1 x) x
    type Foo8 :: Nat -> Nat
    type family Foo8 (a :: Nat) :: Nat where
      Foo8 x = Let0123456789876543210ZSym1 x
    type Foo7 :: Nat -> Nat
    type family Foo7 (a :: Nat) :: Nat where
      Foo7 x = Let0123456789876543210XSym1 x
    type Foo6 :: Nat -> Nat
    type family Foo6 (a :: Nat) :: Nat where
      Foo6 x = Let0123456789876543210ZSym1 x
    type Foo5 :: Nat -> Nat
    type family Foo5 (a :: Nat) :: Nat where
      Foo5 x = Apply (Let0123456789876543210FSym1 x) x
    type Foo4 :: Nat -> Nat
    type family Foo4 (a :: Nat) :: Nat where
      Foo4 x = Apply (Let0123456789876543210FSym1 x) x
    type Foo3 :: Nat -> Nat
    type family Foo3 (a :: Nat) :: Nat where
      Foo3 x = Let0123456789876543210YSym1 x
    type Foo2 :: Nat
    type family Foo2 :: Nat where
      Foo2 = Let0123456789876543210ZSym0
    type Foo1 :: Nat -> Nat
    type family Foo1 (a :: Nat) :: Nat where
      Foo1 x = Let0123456789876543210YSym1 x
    sFoo14 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo14Sym0 t :: (Nat, Nat)) :: Type)
    sFoo13_ ::
      (forall (t :: a). Sing t -> Sing (Apply Foo13_Sym0 t :: a) :: Type)
    sFoo13 ::
      forall a (t :: a). Sing t -> Sing (Apply Foo13Sym0 t :: a)
    sFoo12 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo12Sym0 t :: Nat) :: Type)
    sFoo11 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo11Sym0 t :: Nat) :: Type)
    sFoo10 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo10Sym0 t :: Nat) :: Type)
    sFoo9 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo9Sym0 t :: Nat) :: Type)
    sFoo8 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo8Sym0 t :: Nat) :: Type)
    sFoo7 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo7Sym0 t :: Nat) :: Type)
    sFoo6 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo6Sym0 t :: Nat) :: Type)
    sFoo5 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo5Sym0 t :: Nat) :: Type)
    sFoo4 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo4Sym0 t :: Nat) :: Type)
    sFoo3 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo3Sym0 t :: Nat) :: Type)
    sFoo2 :: (Sing (Foo2Sym0 :: Nat) :: Type)
    sFoo1 ::
      (forall (t :: Nat).
       Sing t -> Sing (Apply Foo1Sym0 t :: Nat) :: Type)
    sFoo14 (sX :: Sing x)
      = let
          sZ :: Sing @_ (Let0123456789876543210ZSym1 x)
          sY :: Sing @_ (Let0123456789876543210YSym1 x)
          sX_0123456789876543210 ::
            Sing @_ (Let0123456789876543210X_0123456789876543210Sym1 x)
          sZ
            = id
                @(Sing (Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)))
                (case sX_0123456789876543210 of
                   STuple2 _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
                     -> sY_0123456789876543210)
          sY
            = id
                @(Sing (Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)))
                (case sX_0123456789876543210 of
                   STuple2 (sY_0123456789876543210 :: Sing y_0123456789876543210) _
                     -> sY_0123456789876543210)
          sX_0123456789876543210
            = applySing
                (applySing
                   (singFun2 @Tuple2Sym0 STuple2)
                   (applySing (singFun1 @SuccSym0 SSucc) sX))
                sX
        in applySing (applySing (singFun2 @Tuple2Sym0 STuple2) sZ) sY
    sFoo13_ (sY :: Sing y) = sY
    sFoo13 (sX :: Sing x)
      = let
          sBar :: (Sing (Let0123456789876543210BarSym1 x :: a) :: Type)
          sBar = sX
        in applySing (singFun1 @Foo13_Sym0 sFoo13_) sBar
    sFoo12 (sX :: Sing x)
      = let
          (%+) ::
            (forall (t :: Nat) (t :: Nat).
             Sing t
             -> Sing t
                -> Sing (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) t) t :: Nat) :: Type)
          (%+) SZero (sM :: Sing m) = sM
          (%+) (SSucc (sN :: Sing n)) (sM :: Sing m)
            = applySing
                (singFun1 @SuccSym0 SSucc)
                (applySing
                   (applySing (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+)) sN)
                   sX)
        in
          applySing
            (applySing (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+)) sX)
            (applySing
               (singFun1 @SuccSym0 SSucc)
               (applySing (singFun1 @SuccSym0 SSucc) SZero))
    sFoo11 (sX :: Sing x)
      = let
          sZ :: (Sing (Let0123456789876543210ZSym1 x :: Nat) :: Type)
          (%+) ::
            (forall (t :: Nat) (t :: Nat).
             Sing t
             -> Sing t
                -> Sing (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) t) t :: Nat) :: Type)
          sZ = sX
          (%+) SZero (sM :: Sing m) = sM
          (%+) (SSucc (sN :: Sing n)) (sM :: Sing m)
            = applySing
                (singFun1 @SuccSym0 SSucc)
                (applySing
                   (applySing (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+)) sN)
                   sM)
        in
          applySing
            (applySing
               (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+))
               (applySing (singFun1 @SuccSym0 SSucc) SZero))
            sZ
    sFoo10 (sX :: Sing x)
      = let
          (%+) ::
            (forall (t :: Nat) (t :: Nat).
             Sing t
             -> Sing t
                -> Sing (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) t) t :: Nat) :: Type)
          (%+) SZero (sM :: Sing m) = sM
          (%+) (SSucc (sN :: Sing n)) (sM :: Sing m)
            = applySing
                (singFun1 @SuccSym0 SSucc)
                (applySing
                   (applySing (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+)) sN)
                   sM)
        in
          applySing
            (applySing
               (singFun2 @((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) (%+))
               (applySing (singFun1 @SuccSym0 SSucc) SZero))
            sX
    sFoo9 (sX :: Sing x)
      = let
          sZ ::
            (forall (t :: Nat).
             Sing t
             -> Sing (Apply (Let0123456789876543210ZSym1 x) t :: Nat) :: Type)
          sZ (sA_0123456789876543210 :: Sing a_0123456789876543210)
            = applySing
                (singFun1
                   @(Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) x)
                   (\ sX -> case sX of (_ :: Sing x) -> sX))
                sA_0123456789876543210
        in applySing (singFun1 @(Let0123456789876543210ZSym1 x) sZ) sX
    sFoo8 (sX :: Sing x)
      = let
          sZ :: (Sing (Let0123456789876543210ZSym1 x :: Nat) :: Type)
          sZ
            = applySing
                (singFun1
                   @(Apply Lambda_0123456789876543210Sym0 x)
                   (\ sX -> case sX of (_ :: Sing x) -> sX))
                SZero
        in sZ
    sFoo7 (sX :: Sing x)
      = let
          sX :: (Sing (Let0123456789876543210XSym1 x :: Nat) :: Type)
          sX = SZero
        in sX
    sFoo6 (sX :: Sing x)
      = let
          sF ::
            (forall (t :: Nat).
             Sing t
             -> Sing (Apply (Let0123456789876543210FSym1 x) t :: Nat) :: Type)
          sF (sY :: Sing y) = applySing (singFun1 @SuccSym0 SSucc) sY in
        let
          sZ :: (Sing (Let0123456789876543210ZSym1 x :: Nat) :: Type)
          sZ = applySing (singFun1 @(Let0123456789876543210FSym1 x) sF) sX
        in sZ
    sFoo5 (sX :: Sing x)
      = let
          sF ::
            (forall (t :: Nat).
             Sing t
             -> Sing (Apply (Let0123456789876543210FSym1 x) t :: Nat) :: Type)
          sF (sY :: Sing y)
            = let
                sZ :: (Sing (Let0123456789876543210ZSym2 y x :: Nat) :: Type)
                sZ = applySing (singFun1 @SuccSym0 SSucc) sY
              in applySing (singFun1 @SuccSym0 SSucc) sZ
        in applySing (singFun1 @(Let0123456789876543210FSym1 x) sF) sX
    sFoo4 (sX :: Sing x)
      = let
          sF ::
            (forall (t :: Nat).
             Sing t
             -> Sing (Apply (Let0123456789876543210FSym1 x) t :: Nat) :: Type)
          sF (sY :: Sing y) = applySing (singFun1 @SuccSym0 SSucc) sY
        in applySing (singFun1 @(Let0123456789876543210FSym1 x) sF) sX
    sFoo3 (sX :: Sing x)
      = let
          sY :: (Sing (Let0123456789876543210YSym1 x :: Nat) :: Type)
          sY = applySing (singFun1 @SuccSym0 SSucc) sX
        in sY
    sFoo2
      = let
          sZ :: Sing @_ Let0123456789876543210ZSym0
          sY :: Sing @_ Let0123456789876543210YSym0
          sZ = applySing (singFun1 @SuccSym0 SSucc) sY
          sY = applySing (singFun1 @SuccSym0 SSucc) SZero
        in sZ
    sFoo1 (sX :: Sing x)
      = let
          sY :: (Sing (Let0123456789876543210YSym1 x :: Nat) :: Type)
          sY = applySing (singFun1 @SuccSym0 SSucc) SZero
        in sY
    instance SingI (Foo14Sym0 :: (~>) Nat (Nat, Nat)) where
      sing = singFun1 @Foo14Sym0 sFoo14
    instance SingI (Foo13_Sym0 :: (~>) a a) where
      sing = singFun1 @Foo13_Sym0 sFoo13_
    instance SingI (Foo13Sym0 :: (~>) a a) where
      sing = singFun1 @Foo13Sym0 sFoo13
    instance SingI (Foo12Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo12Sym0 sFoo12
    instance SingI (Foo11Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo11Sym0 sFoo11
    instance SingI (Foo10Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo10Sym0 sFoo10
    instance SingI (Foo9Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo9Sym0 sFoo9
    instance SingI (Foo8Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo8Sym0 sFoo8
    instance SingI (Foo7Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo7Sym0 sFoo7
    instance SingI (Foo6Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo6Sym0 sFoo6
    instance SingI (Foo5Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo5Sym0 sFoo5
    instance SingI (Foo4Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo4Sym0 sFoo4
    instance SingI (Foo3Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo3Sym0 sFoo3
    instance SingI (Foo1Sym0 :: (~>) Nat Nat) where
      sing = singFun1 @Foo1Sym0 sFoo1