Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| map :: (a -> b) -> [a] -> [b]
          map _ [] = []
          map f (h : t) = (f h) : (map f t)
          liftMaybe :: (a -> b) -> Maybe a -> Maybe b
          liftMaybe f (Just x) = Just (f x)
          liftMaybe _ Nothing = Nothing
          zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
          zipWith f (x : xs) (y : ys) = f x y : zipWith f xs ys
          zipWith _ [] [] = []
          zipWith _ (_ : _) [] = []
          zipWith _ [] (_ : _) = []
          foo :: ((a -> b) -> a -> b) -> (a -> b) -> a -> b
          foo f g a = f g a
          splunge :: [Nat] -> [Bool] -> [Nat]
          splunge ns bs
            = zipWith (\ n b -> if b then Succ (Succ n) else n) ns bs
          etad :: [Nat] -> [Bool] -> [Nat]
          etad = zipWith (\ n b -> if b then Succ (Succ n) else n)
          
          data Either a b = Left a | Right b |]
  ======>
    data Either a b = Left a | Right b
    map :: (a -> b) -> [a] -> [b]
    map _ [] = []
    map f (h : t) = (f h : map f t)
    liftMaybe :: (a -> b) -> Maybe a -> Maybe b
    liftMaybe f (Just x) = Just (f x)
    liftMaybe _ Nothing = Nothing
    zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith f (x : xs) (y : ys) = (f x y : zipWith f xs ys)
    zipWith _ [] [] = []
    zipWith _ (_ : _) [] = []
    zipWith _ [] (_ : _) = []
    foo :: ((a -> b) -> a -> b) -> (a -> b) -> a -> b
    foo f g a = f g a
    splunge :: [Nat] -> [Bool] -> [Nat]
    splunge ns bs
      = zipWith (\ n b -> if b then Succ (Succ n) else n) ns bs
    etad :: [Nat] -> [Bool] -> [Nat]
    etad = zipWith (\ n b -> if b then Succ (Succ n) else n)
    type LeftSym0 :: forall a b. (~>) a (Either a b)
    data LeftSym0 :: (~>) a (Either a b)
      where
        LeftSym0KindInference :: SameKind (Apply LeftSym0 arg) (LeftSym1 arg) =>
                                 LeftSym0 a0123456789876543210
    type instance Apply LeftSym0 a0123456789876543210 = Left a0123456789876543210
    instance SuppressUnusedWarnings LeftSym0 where
      suppressUnusedWarnings = snd ((,) LeftSym0KindInference ())
    type LeftSym1 :: forall a b. a -> Either a b
    type family LeftSym1 (a0123456789876543210 :: a) :: Either a b where
      LeftSym1 a0123456789876543210 = Left a0123456789876543210
    type RightSym0 :: forall a b. (~>) b (Either a b)
    data RightSym0 :: (~>) b (Either a b)
      where
        RightSym0KindInference :: SameKind (Apply RightSym0 arg) (RightSym1 arg) =>
                                  RightSym0 a0123456789876543210
    type instance Apply RightSym0 a0123456789876543210 = Right a0123456789876543210
    instance SuppressUnusedWarnings RightSym0 where
      suppressUnusedWarnings = snd ((,) RightSym0KindInference ())
    type RightSym1 :: forall a b. b -> Either a b
    type family RightSym1 (a0123456789876543210 :: b) :: Either a b where
      RightSym1 a0123456789876543210 = Right a0123456789876543210
    type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where
      Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'True = Apply SuccSym0 (Apply SuccSym0 n)
      Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'False = n
    type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n b where
      Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n b = Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 b
    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 a_01234567898765432100123456789876543210
      where
        Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym1KindInference ())
    data Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210
      where
        Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) n0123456789876543210 = Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym2KindInference ())
    data Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210
      where
        Lambda_0123456789876543210Sym3KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210) arg) (Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210) b0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym3KindInference ())
    type family Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 where
      Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210
    type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 t where
      Case_0123456789876543210 n b ns bs 'True = Apply SuccSym0 (Apply SuccSym0 n)
      Case_0123456789876543210 n b ns bs 'False = n
    type family Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n b where
      Lambda_0123456789876543210 ns bs n b = Case_0123456789876543210 n b ns bs b
    data Lambda_0123456789876543210Sym0 ns0123456789876543210
      where
        Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
                                                       Lambda_0123456789876543210Sym0 ns0123456789876543210
    type instance Apply Lambda_0123456789876543210Sym0 ns0123456789876543210 = Lambda_0123456789876543210Sym1 ns0123456789876543210
    instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym0KindInference ())
    data Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210
      where
        Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 ns0123456789876543210) arg) (Lambda_0123456789876543210Sym2 ns0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym1 ns0123456789876543210) bs0123456789876543210 = Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 ns0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym1KindInference ())
    data Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 n0123456789876543210
      where
        Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210) arg) (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 n0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210) n0123456789876543210 = Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym2KindInference ())
    data Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210
      where
        Lambda_0123456789876543210Sym3KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210) arg) (Lambda_0123456789876543210Sym4 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 arg) =>
                                                       Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210
    type instance Apply (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210) b0123456789876543210 = Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210
    instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 n0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Lambda_0123456789876543210Sym3KindInference ())
    type family Lambda_0123456789876543210Sym4 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 where
      Lambda_0123456789876543210Sym4 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210
    type EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
    data EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
      where
        EtadSym0KindInference :: SameKind (Apply EtadSym0 arg) (EtadSym1 arg) =>
                                 EtadSym0 a0123456789876543210
    type instance Apply EtadSym0 a0123456789876543210 = EtadSym1 a0123456789876543210
    instance SuppressUnusedWarnings EtadSym0 where
      suppressUnusedWarnings = snd ((,) EtadSym0KindInference ())
    type EtadSym1 :: [Nat] -> (~>) [Bool] [Nat]
    data EtadSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
      where
        EtadSym1KindInference :: SameKind (Apply (EtadSym1 a0123456789876543210) arg) (EtadSym2 a0123456789876543210 arg) =>
                                 EtadSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (EtadSym1 a0123456789876543210) a0123456789876543210 = Etad a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (EtadSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) EtadSym1KindInference ())
    type EtadSym2 :: [Nat] -> [Bool] -> [Nat]
    type family EtadSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) :: [Nat] where
      EtadSym2 a0123456789876543210 a0123456789876543210 = Etad a0123456789876543210 a0123456789876543210
    type SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
    data SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
      where
        SplungeSym0KindInference :: SameKind (Apply SplungeSym0 arg) (SplungeSym1 arg) =>
                                    SplungeSym0 a0123456789876543210
    type instance Apply SplungeSym0 a0123456789876543210 = SplungeSym1 a0123456789876543210
    instance SuppressUnusedWarnings SplungeSym0 where
      suppressUnusedWarnings = snd ((,) SplungeSym0KindInference ())
    type SplungeSym1 :: [Nat] -> (~>) [Bool] [Nat]
    data SplungeSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
      where
        SplungeSym1KindInference :: SameKind (Apply (SplungeSym1 a0123456789876543210) arg) (SplungeSym2 a0123456789876543210 arg) =>
                                    SplungeSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (SplungeSym1 a0123456789876543210) a0123456789876543210 = Splunge a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (SplungeSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) SplungeSym1KindInference ())
    type SplungeSym2 :: [Nat] -> [Bool] -> [Nat]
    type family SplungeSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) :: [Nat] where
      SplungeSym2 a0123456789876543210 a0123456789876543210 = Splunge a0123456789876543210 a0123456789876543210
    type FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))
    data FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))
      where
        FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                FooSym0 a0123456789876543210
    type instance Apply FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
    type FooSym1 :: (~>) ((~>) a b) ((~>) a b)
                    -> (~>) ((~>) a b) ((~>) a b)
    data FooSym1 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) :: (~>) ((~>) a b) ((~>) a b)
      where
        FooSym1KindInference :: SameKind (Apply (FooSym1 a0123456789876543210) arg) (FooSym2 a0123456789876543210 arg) =>
                                FooSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (FooSym1 a0123456789876543210) a0123456789876543210 = FooSym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (FooSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) FooSym1KindInference ())
    type FooSym2 :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> (~>) a b
    data FooSym2 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) :: (~>) a b
      where
        FooSym2KindInference :: SameKind (Apply (FooSym2 a0123456789876543210 a0123456789876543210) arg) (FooSym3 a0123456789876543210 a0123456789876543210 arg) =>
                                FooSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (FooSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (FooSym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) FooSym2KindInference ())
    type FooSym3 :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b
    type family FooSym3 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: a) :: b where
      FooSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
    type ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))
    data ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))
      where
        ZipWithSym0KindInference :: SameKind (Apply ZipWithSym0 arg) (ZipWithSym1 arg) =>
                                    ZipWithSym0 a0123456789876543210
    type instance Apply ZipWithSym0 a0123456789876543210 = ZipWithSym1 a0123456789876543210
    instance SuppressUnusedWarnings ZipWithSym0 where
      suppressUnusedWarnings = snd ((,) ZipWithSym0KindInference ())
    type ZipWithSym1 :: (~>) a ((~>) b c) -> (~>) [a] ((~>) [b] [c])
    data ZipWithSym1 (a0123456789876543210 :: (~>) a ((~>) b c)) :: (~>) [a] ((~>) [b] [c])
      where
        ZipWithSym1KindInference :: SameKind (Apply (ZipWithSym1 a0123456789876543210) arg) (ZipWithSym2 a0123456789876543210 arg) =>
                                    ZipWithSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ZipWithSym1 a0123456789876543210) a0123456789876543210 = ZipWithSym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ZipWithSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) ZipWithSym1KindInference ())
    type ZipWithSym2 :: (~>) a ((~>) b c) -> [a] -> (~>) [b] [c]
    data ZipWithSym2 (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) :: (~>) [b] [c]
      where
        ZipWithSym2KindInference :: SameKind (Apply (ZipWithSym2 a0123456789876543210 a0123456789876543210) arg) (ZipWithSym3 a0123456789876543210 a0123456789876543210 arg) =>
                                    ZipWithSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (ZipWithSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ZipWithSym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) ZipWithSym2KindInference ())
    type ZipWithSym3 :: (~>) a ((~>) b c) -> [a] -> [b] -> [c]
    type family ZipWithSym3 (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [c] where
      ZipWithSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
    type LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
    data LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
      where
        LiftMaybeSym0KindInference :: SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
                                      LiftMaybeSym0 a0123456789876543210
    type instance Apply LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
    instance SuppressUnusedWarnings LiftMaybeSym0 where
      suppressUnusedWarnings = snd ((,) LiftMaybeSym0KindInference ())
    type LiftMaybeSym1 :: (~>) a b -> (~>) (Maybe a) (Maybe b)
    data LiftMaybeSym1 (a0123456789876543210 :: (~>) a b) :: (~>) (Maybe a) (Maybe b)
      where
        LiftMaybeSym1KindInference :: SameKind (Apply (LiftMaybeSym1 a0123456789876543210) arg) (LiftMaybeSym2 a0123456789876543210 arg) =>
                                      LiftMaybeSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) LiftMaybeSym1KindInference ())
    type LiftMaybeSym2 :: (~>) a b -> Maybe a -> Maybe b
    type family LiftMaybeSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where
      LiftMaybeSym2 a0123456789876543210 a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
    type MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])
    data MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])
      where
        MapSym0KindInference :: SameKind (Apply MapSym0 arg) (MapSym1 arg) =>
                                MapSym0 a0123456789876543210
    type instance Apply MapSym0 a0123456789876543210 = MapSym1 a0123456789876543210
    instance SuppressUnusedWarnings MapSym0 where
      suppressUnusedWarnings = snd ((,) MapSym0KindInference ())
    type MapSym1 :: (~>) a b -> (~>) [a] [b]
    data MapSym1 (a0123456789876543210 :: (~>) a b) :: (~>) [a] [b]
      where
        MapSym1KindInference :: SameKind (Apply (MapSym1 a0123456789876543210) arg) (MapSym2 a0123456789876543210 arg) =>
                                MapSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (MapSym1 a0123456789876543210) a0123456789876543210 = Map a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MapSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MapSym1KindInference ())
    type MapSym2 :: (~>) a b -> [a] -> [b]
    type family MapSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: [a]) :: [b] where
      MapSym2 a0123456789876543210 a0123456789876543210 = Map a0123456789876543210 a0123456789876543210
    type Etad :: [Nat] -> [Bool] -> [Nat]
    type family Etad (a :: [Nat]) (a :: [Bool]) :: [Nat] where
      Etad a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210)) a_0123456789876543210) a_0123456789876543210
    type Splunge :: [Nat] -> [Bool] -> [Nat]
    type family Splunge (a :: [Nat]) (a :: [Bool]) :: [Nat] where
      Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789876543210Sym0 ns) bs)) ns) bs
    type Foo :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b
    type family Foo (a :: (~>) ((~>) a b) ((~>) a b)) (a :: (~>) a b) (a :: a) :: b where
      Foo f g a = Apply (Apply f g) a
    type ZipWith :: (~>) a ((~>) b c) -> [a] -> [b] -> [c]
    type family ZipWith (a :: (~>) a ((~>) b c)) (a :: [a]) (a :: [b]) :: [c] where
      ZipWith f ('(:) x xs) ('(:) y ys) = Apply (Apply (:@#@$) (Apply (Apply f x) y)) (Apply (Apply (Apply ZipWithSym0 f) xs) ys)
      ZipWith _ '[] '[] = NilSym0
      ZipWith _ ('(:) _ _) '[] = NilSym0
      ZipWith _ '[] ('(:) _ _) = NilSym0
    type LiftMaybe :: (~>) a b -> Maybe a -> Maybe b
    type family LiftMaybe (a :: (~>) a b) (a :: Maybe a) :: Maybe b where
      LiftMaybe f ('Just x) = Apply JustSym0 (Apply f x)
      LiftMaybe _ 'Nothing = NothingSym0
    type Map :: (~>) a b -> [a] -> [b]
    type family Map (a :: (~>) a b) (a :: [a]) :: [b] where
      Map _ '[] = NilSym0
      Map f ('(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t)
    sEtad ::
      (forall (t :: [Nat]) (t :: [Bool]).
       Sing t
       -> Sing t -> Sing (Apply (Apply EtadSym0 t) t :: [Nat]) :: Type)
    sSplunge ::
      (forall (t :: [Nat]) (t :: [Bool]).
       Sing t
       -> Sing t -> Sing (Apply (Apply SplungeSym0 t) t :: [Nat]) :: Type)
    sFoo ::
      (forall (t :: (~>) ((~>) a b) ((~>) a b)) (t :: (~>) a b) (t :: a).
       Sing t
       -> Sing t
          -> Sing t
             -> Sing (Apply (Apply (Apply FooSym0 t) t) t :: b) :: Type)
    sZipWith ::
      (forall (t :: (~>) a ((~>) b c)) (t :: [a]) (t :: [b]).
       Sing t
       -> Sing t
          -> Sing t
             -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c]) :: Type)
    sLiftMaybe ::
      (forall (t :: (~>) a b) (t :: Maybe a).
       Sing t
       -> Sing t
          -> Sing (Apply (Apply LiftMaybeSym0 t) t :: Maybe b) :: Type)
    sMap ::
      (forall (t :: (~>) a b) (t :: [a]).
       Sing t
       -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) :: Type)
    sEtad
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = applySing
          (applySing
             (applySing
                (singFun3 @ZipWithSym0 sZipWith)
                (singFun2
                   @(Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210)
                   (\ sN sB
                      -> case (,) sN sB of
                           (,) (_ :: Sing n) (_ :: Sing b)
                             -> id
                                  @(Sing (Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 b))
                                  (case sB of
                                     STrue
                                       -> applySing
                                            (singFun1 @SuccSym0 SSucc)
                                            (applySing (singFun1 @SuccSym0 SSucc) sN)
                                     SFalse -> sN))))
             sA_0123456789876543210)
          sA_0123456789876543210
    sSplunge (sNs :: Sing ns) (sBs :: Sing bs)
      = applySing
          (applySing
             (applySing
                (singFun3 @ZipWithSym0 sZipWith)
                (singFun2
                   @(Apply (Apply Lambda_0123456789876543210Sym0 ns) bs)
                   (\ sN sB
                      -> case (,) sN sB of
                           (,) (_ :: Sing n) (_ :: Sing b)
                             -> id
                                  @(Sing (Case_0123456789876543210 n b ns bs b))
                                  (case sB of
                                     STrue
                                       -> applySing
                                            (singFun1 @SuccSym0 SSucc)
                                            (applySing (singFun1 @SuccSym0 SSucc) sN)
                                     SFalse -> sN))))
             sNs)
          sBs
    sFoo (sF :: Sing f) (sG :: Sing g) (sA :: Sing a)
      = applySing (applySing sF sG) sA
    sZipWith
      (sF :: Sing f)
      (SCons (sX :: Sing x) (sXs :: Sing xs))
      (SCons (sY :: Sing y) (sYs :: Sing ys))
      = applySing
          (applySing
             (singFun2 @(:@#@$) SCons) (applySing (applySing sF sX) sY))
          (applySing
             (applySing (applySing (singFun3 @ZipWithSym0 sZipWith) sF) sXs)
             sYs)
    sZipWith _ SNil SNil = SNil
    sZipWith _ (SCons _ _) SNil = SNil
    sZipWith _ SNil (SCons _ _) = SNil
    sLiftMaybe (sF :: Sing f) (SJust (sX :: Sing x))
      = applySing (singFun1 @JustSym0 SJust) (applySing sF sX)
    sLiftMaybe _ SNothing = SNothing
    sMap _ SNil = SNil
    sMap (sF :: Sing f) (SCons (sH :: Sing h) (sT :: Sing t))
      = applySing
          (applySing (singFun2 @(:@#@$) SCons) (applySing sF sH))
          (applySing (applySing (singFun2 @MapSym0 sMap) sF) sT)
    instance SingI (EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])) where
      sing = singFun2 @EtadSym0 sEtad
    instance SingI d =>
             SingI (EtadSym1 (d :: [Nat]) :: (~>) [Bool] [Nat]) where
      sing = singFun1 @(EtadSym1 (d :: [Nat])) (sEtad (sing @d))
    instance SingI1 (EtadSym1 :: [Nat] -> (~>) [Bool] [Nat]) where
      liftSing (s :: Sing (d :: [Nat]))
        = singFun1 @(EtadSym1 (d :: [Nat])) (sEtad s)
    instance SingI (SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])) where
      sing = singFun2 @SplungeSym0 sSplunge
    instance SingI d =>
             SingI (SplungeSym1 (d :: [Nat]) :: (~>) [Bool] [Nat]) where
      sing = singFun1 @(SplungeSym1 (d :: [Nat])) (sSplunge (sing @d))
    instance SingI1 (SplungeSym1 :: [Nat] -> (~>) [Bool] [Nat]) where
      liftSing (s :: Sing (d :: [Nat]))
        = singFun1 @(SplungeSym1 (d :: [Nat])) (sSplunge s)
    instance SingI (FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))) where
      sing = singFun3 @FooSym0 sFoo
    instance SingI d =>
             SingI (FooSym1 (d :: (~>) ((~>) a b) ((~>) a b)) :: (~>) ((~>) a b) ((~>) a b)) where
      sing
        = singFun2
            @(FooSym1 (d :: (~>) ((~>) a b) ((~>) a b))) (sFoo (sing @d))
    instance SingI1 (FooSym1 :: (~>) ((~>) a b) ((~>) a b)
                                -> (~>) ((~>) a b) ((~>) a b)) where
      liftSing (s :: Sing (d :: (~>) ((~>) a b) ((~>) a b)))
        = singFun2 @(FooSym1 (d :: (~>) ((~>) a b) ((~>) a b))) (sFoo s)
    instance (SingI d, SingI d) =>
             SingI (FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b) :: (~>) a b) where
      sing
        = singFun1
            @(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b))
            (sFoo (sing @d) (sing @d))
    instance SingI d =>
             SingI1 (FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) :: (~>) a b
                                                                  -> (~>) a b) where
      liftSing (s :: Sing (d :: (~>) a b))
        = singFun1
            @(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b))
            (sFoo (sing @d) s)
    instance SingI2 (FooSym2 :: (~>) ((~>) a b) ((~>) a b)
                                -> (~>) a b -> (~>) a b) where
      liftSing2
        (s :: Sing (d :: (~>) ((~>) a b) ((~>) a b)))
        (s :: Sing (d :: (~>) a b))
        = singFun1
            @(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b))
            (sFoo s s)
    instance SingI (ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))) where
      sing = singFun3 @ZipWithSym0 sZipWith
    instance SingI d =>
             SingI (ZipWithSym1 (d :: (~>) a ((~>) b c)) :: (~>) [a] ((~>) [b] [c])) where
      sing
        = singFun2
            @(ZipWithSym1 (d :: (~>) a ((~>) b c))) (sZipWith (sing @d))
    instance SingI1 (ZipWithSym1 :: (~>) a ((~>) b c)
                                    -> (~>) [a] ((~>) [b] [c])) where
      liftSing (s :: Sing (d :: (~>) a ((~>) b c)))
        = singFun2 @(ZipWithSym1 (d :: (~>) a ((~>) b c))) (sZipWith s)
    instance (SingI d, SingI d) =>
             SingI (ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a]) :: (~>) [b] [c]) where
      sing
        = singFun1
            @(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a]))
            (sZipWith (sing @d) (sing @d))
    instance SingI d =>
             SingI1 (ZipWithSym2 (d :: (~>) a ((~>) b c)) :: [a]
                                                             -> (~>) [b] [c]) where
      liftSing (s :: Sing (d :: [a]))
        = singFun1
            @(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a]))
            (sZipWith (sing @d) s)
    instance SingI2 (ZipWithSym2 :: (~>) a ((~>) b c)
                                    -> [a] -> (~>) [b] [c]) where
      liftSing2
        (s :: Sing (d :: (~>) a ((~>) b c)))
        (s :: Sing (d :: [a]))
        = singFun1
            @(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a])) (sZipWith s s)
    instance SingI (LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))) where
      sing = singFun2 @LiftMaybeSym0 sLiftMaybe
    instance SingI d =>
             SingI (LiftMaybeSym1 (d :: (~>) a b) :: (~>) (Maybe a) (Maybe b)) where
      sing
        = singFun1 @(LiftMaybeSym1 (d :: (~>) a b)) (sLiftMaybe (sing @d))
    instance SingI1 (LiftMaybeSym1 :: (~>) a b
                                      -> (~>) (Maybe a) (Maybe b)) where
      liftSing (s :: Sing (d :: (~>) a b))
        = singFun1 @(LiftMaybeSym1 (d :: (~>) a b)) (sLiftMaybe s)
    instance SingI (MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])) where
      sing = singFun2 @MapSym0 sMap
    instance SingI d =>
             SingI (MapSym1 (d :: (~>) a b) :: (~>) [a] [b]) where
      sing = singFun1 @(MapSym1 (d :: (~>) a b)) (sMap (sing @d))
    instance SingI1 (MapSym1 :: (~>) a b -> (~>) [a] [b]) where
      liftSing (s :: Sing (d :: (~>) a b))
        = singFun1 @(MapSym1 (d :: (~>) a b)) (sMap s)
    data SEither :: forall a b. Either a b -> Type
      where
        SLeft :: forall a b (n :: a).
                 (Sing n) -> SEither (Left n :: Either a b)
        SRight :: forall a b (n :: b).
                  (Sing n) -> SEither (Right n :: Either a b)
    type instance Sing @(Either a b) = SEither
    instance (SingKind a, SingKind b) => SingKind (Either a b) where
      type Demote (Either a b) = Either (Demote a) (Demote b)
      fromSing (SLeft b) = Left (fromSing b)
      fromSing (SRight b) = Right (fromSing b)
      toSing (Left (b :: Demote a))
        = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SLeft c)
      toSing (Right (b :: Demote b))
        = case toSing b :: SomeSing b of SomeSing c -> SomeSing (SRight c)
    instance SingI n => SingI (Left (n :: a)) where
      sing = SLeft sing
    instance SingI1 Left where
      liftSing = SLeft
    instance SingI (LeftSym0 :: (~>) a (Either a b)) where
      sing = singFun1 @LeftSym0 SLeft
    instance SingI n => SingI (Right (n :: b)) where
      sing = SRight sing
    instance SingI1 Right where
      liftSing = SRight
    instance SingI (RightSym0 :: (~>) b (Either a b)) where
      sing = singFun1 @RightSym0 SRight