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 :: forall a b. (a -> b) -> [a] -> [b]
    map _ GHC.Types.[] = []
    map f (h GHC.Types.: t) = ((f h) GHC.Types.: (map f t))
    liftMaybe :: forall a b. (a -> b) -> Maybe a -> Maybe b
    liftMaybe f (Just x) = Just (f x)
    liftMaybe _ Nothing = Nothing
    zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith f (x GHC.Types.: xs) (y GHC.Types.: ys)
      = ((f x y) GHC.Types.: (zipWith f xs ys))
    zipWith _ GHC.Types.[] GHC.Types.[] = []
    zipWith _ (_ GHC.Types.: _) GHC.Types.[] = []
    zipWith _ GHC.Types.[] (_ GHC.Types.: _) = []
    foo :: forall a b. ((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 LeftSym1 (t :: a) = Left t
    instance SuppressUnusedWarnings LeftSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) LeftSym0KindInference GHC.Tuple.())
    data LeftSym0 (l :: TyFun a (Either a b))
      = forall arg. KindOf (Apply LeftSym0 arg) ~ KindOf (LeftSym1 arg) =>
        LeftSym0KindInference
    type instance Apply LeftSym0 l = LeftSym1 l
    type RightSym1 (t :: b) = Right t
    instance SuppressUnusedWarnings RightSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) RightSym0KindInference GHC.Tuple.())
    data RightSym0 (l :: TyFun b (Either a b))
      = forall arg. KindOf (Apply RightSym0 arg) ~ KindOf (RightSym1 arg) =>
        RightSym0KindInference
    type instance Apply RightSym0 l = RightSym1 l
    type Let0123456789Scrutinee_0123456789Sym4 t t t t =
        Let0123456789Scrutinee_0123456789 t t t t
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym3 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym3KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym3 l l l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym3 l l l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym4 l l l arg) =>
        Let0123456789Scrutinee_0123456789Sym3KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym3 l l l) l = Let0123456789Scrutinee_0123456789Sym4 l l l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym2 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym2 l l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym2 l l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym3 l l arg) =>
        Let0123456789Scrutinee_0123456789Sym2KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym2 l l) l = Let0123456789Scrutinee_0123456789Sym3 l l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym1 l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym2 l arg) =>
        Let0123456789Scrutinee_0123456789Sym1KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym1 l) l = Let0123456789Scrutinee_0123456789Sym2 l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym0 l
      = forall arg. KindOf (Apply Let0123456789Scrutinee_0123456789Sym0 arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym1 arg) =>
        Let0123456789Scrutinee_0123456789Sym0KindInference
    type instance Apply Let0123456789Scrutinee_0123456789Sym0 l = Let0123456789Scrutinee_0123456789Sym1 l
    type family Let0123456789Scrutinee_0123456789 ns bs n b where
      Let0123456789Scrutinee_0123456789 ns bs n b = b
    type family Case_0123456789 ns bs n b t where
      Case_0123456789 ns bs n b True = Apply SuccSym0 (Apply SuccSym0 n)
      Case_0123456789 ns bs n b False = n
    type family Lambda_0123456789 ns bs t t where
      Lambda_0123456789 ns bs n b = Case_0123456789 ns bs n b (Let0123456789Scrutinee_0123456789Sym4 ns bs n b)
    type Lambda_0123456789Sym4 t t t t = Lambda_0123456789 t t t t
    instance SuppressUnusedWarnings Lambda_0123456789Sym3 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym3KindInference GHC.Tuple.())
    data Lambda_0123456789Sym3 l l l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym3 l l l) arg) ~ KindOf (Lambda_0123456789Sym4 l l l arg) =>
        Lambda_0123456789Sym3KindInference
    type instance Apply (Lambda_0123456789Sym3 l l l) l = Lambda_0123456789Sym4 l l l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
    data Lambda_0123456789Sym2 l l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) =>
        Lambda_0123456789Sym2KindInference
    type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
    data Lambda_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
        Lambda_0123456789Sym1KindInference
    type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
    data Lambda_0123456789Sym0 l
      = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
        Lambda_0123456789Sym0KindInference
    type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
    type Let0123456789Scrutinee_0123456789Sym4 t t t t =
        Let0123456789Scrutinee_0123456789 t t t t
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym3 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym3KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym3 l l l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym3 l l l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym4 l l l arg) =>
        Let0123456789Scrutinee_0123456789Sym3KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym3 l l l) l = Let0123456789Scrutinee_0123456789Sym4 l l l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym2 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym2 l l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym2 l l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym3 l l arg) =>
        Let0123456789Scrutinee_0123456789Sym2KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym2 l l) l = Let0123456789Scrutinee_0123456789Sym3 l l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym1 l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym2 l arg) =>
        Let0123456789Scrutinee_0123456789Sym1KindInference
    type instance Apply (Let0123456789Scrutinee_0123456789Sym1 l) l = Let0123456789Scrutinee_0123456789Sym2 l l
    instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
    data Let0123456789Scrutinee_0123456789Sym0 l
      = forall arg. KindOf (Apply Let0123456789Scrutinee_0123456789Sym0 arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym1 arg) =>
        Let0123456789Scrutinee_0123456789Sym0KindInference
    type instance Apply Let0123456789Scrutinee_0123456789Sym0 l = Let0123456789Scrutinee_0123456789Sym1 l
    type family Let0123456789Scrutinee_0123456789 n
                                                  b
                                                  a_0123456789
                                                  a_0123456789 where
      Let0123456789Scrutinee_0123456789 n b a_0123456789 a_0123456789 = b
    type family Case_0123456789 n b a_0123456789 a_0123456789 t where
      Case_0123456789 n b a_0123456789 a_0123456789 True = Apply SuccSym0 (Apply SuccSym0 n)
      Case_0123456789 n b a_0123456789 a_0123456789 False = n
    type family Lambda_0123456789 a_0123456789 a_0123456789 t t where
      Lambda_0123456789 a_0123456789 a_0123456789 n b = Case_0123456789 n b a_0123456789 a_0123456789 (Let0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789)
    type Lambda_0123456789Sym4 t t t t = Lambda_0123456789 t t t t
    instance SuppressUnusedWarnings Lambda_0123456789Sym3 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym3KindInference GHC.Tuple.())
    data Lambda_0123456789Sym3 l l l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym3 l l l) arg) ~ KindOf (Lambda_0123456789Sym4 l l l arg) =>
        Lambda_0123456789Sym3KindInference
    type instance Apply (Lambda_0123456789Sym3 l l l) l = Lambda_0123456789Sym4 l l l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
    data Lambda_0123456789Sym2 l l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) =>
        Lambda_0123456789Sym2KindInference
    type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
    data Lambda_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
        Lambda_0123456789Sym1KindInference
    type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
    data Lambda_0123456789Sym0 l
      = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
        Lambda_0123456789Sym0KindInference
    type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
    type FooSym3 (t :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
                 (t :: TyFun a b -> *)
                 (t :: a) =
        Foo t t t
    instance SuppressUnusedWarnings FooSym2 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) FooSym2KindInference GHC.Tuple.())
    data FooSym2 (l :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
                 (l :: TyFun a b -> *)
                 (l :: TyFun a b)
      = forall arg. KindOf (Apply (FooSym2 l l) arg) ~ KindOf (FooSym3 l l arg) =>
        FooSym2KindInference
    type instance Apply (FooSym2 l l) l = FooSym3 l l l
    instance SuppressUnusedWarnings FooSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) FooSym1KindInference GHC.Tuple.())
    data FooSym1 (l :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
                 (l :: TyFun (TyFun a b -> *) (TyFun a b -> *))
      = forall arg. KindOf (Apply (FooSym1 l) arg) ~ KindOf (FooSym2 l arg) =>
        FooSym1KindInference
    type instance Apply (FooSym1 l) l = FooSym2 l l
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) FooSym0KindInference GHC.Tuple.())
    data FooSym0 (l :: TyFun (TyFun (TyFun a b -> *) (TyFun a b -> *)
                              -> *) (TyFun (TyFun a b -> *) (TyFun a b -> *) -> *))
      = forall arg. KindOf (Apply FooSym0 arg) ~ KindOf (FooSym1 arg) =>
        FooSym0KindInference
    type instance Apply FooSym0 l = FooSym1 l
    type ZipWithSym3 (t :: TyFun a (TyFun b c -> *) -> *)
                     (t :: [a])
                     (t :: [b]) =
        ZipWith t t t
    instance SuppressUnusedWarnings ZipWithSym2 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ZipWithSym2KindInference GHC.Tuple.())
    data ZipWithSym2 (l :: TyFun a (TyFun b c -> *) -> *)
                     (l :: [a])
                     (l :: TyFun [b] [c])
      = forall arg. KindOf (Apply (ZipWithSym2 l l) arg) ~ KindOf (ZipWithSym3 l l arg) =>
        ZipWithSym2KindInference
    type instance Apply (ZipWithSym2 l l) l = ZipWithSym3 l l l
    instance SuppressUnusedWarnings ZipWithSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ZipWithSym1KindInference GHC.Tuple.())
    data ZipWithSym1 (l :: TyFun a (TyFun b c -> *) -> *)
                     (l :: TyFun [a] (TyFun [b] [c] -> *))
      = forall arg. KindOf (Apply (ZipWithSym1 l) arg) ~ KindOf (ZipWithSym2 l arg) =>
        ZipWithSym1KindInference
    type instance Apply (ZipWithSym1 l) l = ZipWithSym2 l l
    instance SuppressUnusedWarnings ZipWithSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ZipWithSym0KindInference GHC.Tuple.())
    data ZipWithSym0 (l :: TyFun (TyFun a (TyFun b c -> *)
                                  -> *) (TyFun [a] (TyFun [b] [c] -> *) -> *))
      = forall arg. KindOf (Apply ZipWithSym0 arg) ~ KindOf (ZipWithSym1 arg) =>
        ZipWithSym0KindInference
    type instance Apply ZipWithSym0 l = ZipWithSym1 l
    type SplungeSym2 (t :: [Nat]) (t :: [Bool]) = Splunge t t
    instance SuppressUnusedWarnings SplungeSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) SplungeSym1KindInference GHC.Tuple.())
    data SplungeSym1 (l :: [Nat]) (l :: TyFun [Bool] [Nat])
      = forall arg. KindOf (Apply (SplungeSym1 l) arg) ~ KindOf (SplungeSym2 l arg) =>
        SplungeSym1KindInference
    type instance Apply (SplungeSym1 l) l = SplungeSym2 l l
    instance SuppressUnusedWarnings SplungeSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) SplungeSym0KindInference GHC.Tuple.())
    data SplungeSym0 (l :: TyFun [Nat] (TyFun [Bool] [Nat] -> *))
      = forall arg. KindOf (Apply SplungeSym0 arg) ~ KindOf (SplungeSym1 arg) =>
        SplungeSym0KindInference
    type instance Apply SplungeSym0 l = SplungeSym1 l
    type EtadSym2 (t :: [Nat]) (t :: [Bool]) = Etad t t
    instance SuppressUnusedWarnings EtadSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) EtadSym1KindInference GHC.Tuple.())
    data EtadSym1 (l :: [Nat]) (l :: TyFun [Bool] [Nat])
      = forall arg. KindOf (Apply (EtadSym1 l) arg) ~ KindOf (EtadSym2 l arg) =>
        EtadSym1KindInference
    type instance Apply (EtadSym1 l) l = EtadSym2 l l
    instance SuppressUnusedWarnings EtadSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) EtadSym0KindInference GHC.Tuple.())
    data EtadSym0 (l :: TyFun [Nat] (TyFun [Bool] [Nat] -> *))
      = forall arg. KindOf (Apply EtadSym0 arg) ~ KindOf (EtadSym1 arg) =>
        EtadSym0KindInference
    type instance Apply EtadSym0 l = EtadSym1 l
    type LiftMaybeSym2 (t :: TyFun a b -> *) (t :: Maybe a) =
        LiftMaybe t t
    instance SuppressUnusedWarnings LiftMaybeSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) LiftMaybeSym1KindInference GHC.Tuple.())
    data LiftMaybeSym1 (l :: TyFun a b -> *)
                       (l :: TyFun (Maybe a) (Maybe b))
      = forall arg. KindOf (Apply (LiftMaybeSym1 l) arg) ~ KindOf (LiftMaybeSym2 l arg) =>
        LiftMaybeSym1KindInference
    type instance Apply (LiftMaybeSym1 l) l = LiftMaybeSym2 l l
    instance SuppressUnusedWarnings LiftMaybeSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) LiftMaybeSym0KindInference GHC.Tuple.())
    data LiftMaybeSym0 (l :: TyFun (TyFun a b
                                    -> *) (TyFun (Maybe a) (Maybe b) -> *))
      = forall arg. KindOf (Apply LiftMaybeSym0 arg) ~ KindOf (LiftMaybeSym1 arg) =>
        LiftMaybeSym0KindInference
    type instance Apply LiftMaybeSym0 l = LiftMaybeSym1 l
    type MapSym2 (t :: TyFun a b -> *) (t :: [a]) = Map t t
    instance SuppressUnusedWarnings MapSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) MapSym1KindInference GHC.Tuple.())
    data MapSym1 (l :: TyFun a b -> *) (l :: TyFun [a] [b])
      = forall arg. KindOf (Apply (MapSym1 l) arg) ~ KindOf (MapSym2 l arg) =>
        MapSym1KindInference
    type instance Apply (MapSym1 l) l = MapSym2 l l
    instance SuppressUnusedWarnings MapSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) MapSym0KindInference GHC.Tuple.())
    data MapSym0 (l :: TyFun (TyFun a b -> *) (TyFun [a] [b] -> *))
      = forall arg. KindOf (Apply MapSym0 arg) ~ KindOf (MapSym1 arg) =>
        MapSym0KindInference
    type instance Apply MapSym0 l = MapSym1 l
    type family Foo (a :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
                    (a :: TyFun a b -> *)
                    (a :: a) :: b where
      Foo f g a = Apply (Apply f g) a
    type family ZipWith (a :: TyFun a (TyFun 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 _z_0123456789 '[] '[] = '[]
      ZipWith _z_0123456789 ((:) _z_0123456789 _z_0123456789) '[] = '[]
      ZipWith _z_0123456789 '[] ((:) _z_0123456789 _z_0123456789) = '[]
    type family Splunge (a :: [Nat]) (a :: [Bool]) :: [Nat] where
      Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789Sym0 ns) bs)) ns) bs
    type family Etad (a :: [Nat]) (a :: [Bool]) :: [Nat] where
      Etad a_0123456789 a_0123456789 = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789)) a_0123456789) a_0123456789
    type family LiftMaybe (a :: TyFun a b -> *)
                          (a :: Maybe a) :: Maybe b where
      LiftMaybe f (Just x) = Apply JustSym0 (Apply f x)
      LiftMaybe _z_0123456789 Nothing = NothingSym0
    type family Map (a :: TyFun a b -> *) (a :: [a]) :: [b] where
      Map _z_0123456789 '[] = '[]
      Map f ((:) h t) = Apply (Apply (:$) (Apply f h)) (Apply (Apply MapSym0 f) t)
    sFoo ::
      forall (t :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
             (t :: TyFun a b -> *)
             (t :: a).
      Sing t
      -> Sing t
         -> Sing t -> Sing (Apply (Apply (Apply FooSym0 t) t) t :: b)
    sZipWith ::
      forall (t :: TyFun a (TyFun b c -> *) -> *) (t :: [a]) (t :: [b]).
      Sing t
      -> Sing t
         -> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c])
    sSplunge ::
      forall (t :: [Nat]) (t :: [Bool]).
      Sing t -> Sing t -> Sing (Apply (Apply SplungeSym0 t) t :: [Nat])
    sEtad ::
      forall (t :: [Nat]) (t :: [Bool]).
      Sing t -> Sing t -> Sing (Apply (Apply EtadSym0 t) t :: [Nat])
    sLiftMaybe ::
      forall (t :: TyFun a b -> *) (t :: Maybe a).
      Sing t
      -> Sing t -> Sing (Apply (Apply LiftMaybeSym0 t) t :: Maybe b)
    sMap ::
      forall (t :: TyFun a b -> *) (t :: [a]).
      Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b])
    sFoo sF sG sA
      = let
          lambda ::
            forall f g a. (t ~ f, t ~ g, t ~ a) =>
            Sing f
            -> Sing g
               -> Sing a -> Sing (Apply (Apply (Apply FooSym0 f) g) a :: b)
          lambda f g a = applySing (applySing f g) a
        in lambda sF sG sA
    sZipWith sF (SCons sX sXs) (SCons sY sYs)
      = let
          lambda ::
            forall f x xs y ys. (t ~ f,
                                 t ~ Apply (Apply (:$) x) xs,
                                 t ~ Apply (Apply (:$) y) ys) =>
            Sing f
            -> Sing x
               -> Sing xs
                  -> Sing y
                     -> Sing ys
                        -> Sing (Apply (Apply (Apply ZipWithSym0 f) (Apply (Apply (:$) x) xs)) (Apply (Apply (:$) y) ys) :: [c])
          lambda f x xs y ys
            = applySing
                (applySing
                   (singFun2 (Proxy :: Proxy (:$)) SCons)
                   (applySing (applySing f x) y))
                (applySing
                   (applySing
                      (applySing (singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith) f) xs)
                   ys)
        in lambda sF sX sXs sY sYs
    sZipWith _s_z_0123456789 SNil SNil
      = let
          lambda ::
            forall _z_0123456789. (t ~ _z_0123456789, t ~ '[], t ~ '[]) =>
            Sing _z_0123456789
            -> Sing (Apply (Apply (Apply ZipWithSym0 _z_0123456789) '[]) '[] :: [c])
          lambda _z_0123456789 = SNil
        in lambda _s_z_0123456789
    sZipWith
      _s_z_0123456789
      (SCons _s_z_0123456789 _s_z_0123456789)
      SNil
      = let
          lambda ::
            forall _z_0123456789
                   _z_0123456789
                   _z_0123456789. (t ~ _z_0123456789,
                                   t ~ Apply (Apply (:$) _z_0123456789) _z_0123456789,
                                   t ~ '[]) =>
            Sing _z_0123456789
            -> Sing _z_0123456789
               -> Sing _z_0123456789
                  -> Sing (Apply (Apply (Apply ZipWithSym0 _z_0123456789) (Apply (Apply (:$) _z_0123456789) _z_0123456789)) '[] :: [c])
          lambda _z_0123456789 _z_0123456789 _z_0123456789 = SNil
        in lambda _s_z_0123456789 _s_z_0123456789 _s_z_0123456789
    sZipWith
      _s_z_0123456789
      SNil
      (SCons _s_z_0123456789 _s_z_0123456789)
      = let
          lambda ::
            forall _z_0123456789
                   _z_0123456789
                   _z_0123456789. (t ~ _z_0123456789,
                                   t ~ '[],
                                   t ~ Apply (Apply (:$) _z_0123456789) _z_0123456789) =>
            Sing _z_0123456789
            -> Sing _z_0123456789
               -> Sing _z_0123456789
                  -> Sing (Apply (Apply (Apply ZipWithSym0 _z_0123456789) '[]) (Apply (Apply (:$) _z_0123456789) _z_0123456789) :: [c])
          lambda _z_0123456789 _z_0123456789 _z_0123456789 = SNil
        in lambda _s_z_0123456789 _s_z_0123456789 _s_z_0123456789
    sSplunge sNs sBs
      = let
          lambda ::
            forall ns bs. (t ~ ns, t ~ bs) =>
            Sing ns
            -> Sing bs -> Sing (Apply (Apply SplungeSym0 ns) bs :: [Nat])
          lambda ns bs
            = applySing
                (applySing
                   (applySing
                      (singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith)
                      (singFun2
                         (Proxy :: Proxy (Apply (Apply Lambda_0123456789Sym0 ns) bs))
                         (\ sN sB
                            -> let
                                 lambda ::
                                   forall n b.
                                   Sing n
                                   -> Sing b
                                      -> Sing (Apply (Apply (Apply (Apply Lambda_0123456789Sym0 ns) bs) n) b)
                                 lambda n b
                                   = let
                                       sScrutinee_0123456789 ::
                                         Sing (Let0123456789Scrutinee_0123456789Sym4 ns bs n b)
                                       sScrutinee_0123456789 = b
                                     in  case sScrutinee_0123456789 of {
                                           STrue
                                             -> let
                                                  lambda ::
                                                    TrueSym0 ~ Let0123456789Scrutinee_0123456789Sym4 ns bs n b =>
                                                    Sing (Case_0123456789 ns bs n b TrueSym0)
                                                  lambda
                                                    = applySing
                                                        (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                                                        (applySing
                                                           (singFun1
                                                              (Proxy :: Proxy SuccSym0) SSucc)
                                                           n)
                                                in lambda
                                           SFalse
                                             -> let
                                                  lambda ::
                                                    FalseSym0 ~ Let0123456789Scrutinee_0123456789Sym4 ns bs n b =>
                                                    Sing (Case_0123456789 ns bs n b FalseSym0)
                                                  lambda = n
                                                in lambda } ::
                                           Sing (Case_0123456789 ns bs n b (Let0123456789Scrutinee_0123456789Sym4 ns bs n b))
                               in lambda sN sB)))
                   ns)
                bs
        in lambda sNs sBs
    sEtad sA_0123456789 sA_0123456789
      = let
          lambda ::
            forall a_0123456789 a_0123456789. (t ~ a_0123456789,
                                               t ~ a_0123456789) =>
            Sing a_0123456789
            -> Sing a_0123456789
               -> Sing (Apply (Apply EtadSym0 a_0123456789) a_0123456789 :: [Nat])
          lambda a_0123456789 a_0123456789
            = applySing
                (applySing
                   (applySing
                      (singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith)
                      (singFun2
                         (Proxy ::
                            Proxy (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789))
                         (\ sN sB
                            -> let
                                 lambda ::
                                   forall n b.
                                   Sing n
                                   -> Sing b
                                      -> Sing (Apply (Apply (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789) n) b)
                                 lambda n b
                                   = let
                                       sScrutinee_0123456789 ::
                                         Sing (Let0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789)
                                       sScrutinee_0123456789 = b
                                     in  case sScrutinee_0123456789 of {
                                           STrue
                                             -> let
                                                  lambda ::
                                                    TrueSym0 ~ Let0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789 =>
                                                    Sing (Case_0123456789 n b a_0123456789 a_0123456789 TrueSym0)
                                                  lambda
                                                    = applySing
                                                        (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                                                        (applySing
                                                           (singFun1
                                                              (Proxy :: Proxy SuccSym0) SSucc)
                                                           n)
                                                in lambda
                                           SFalse
                                             -> let
                                                  lambda ::
                                                    FalseSym0 ~ Let0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789 =>
                                                    Sing (Case_0123456789 n b a_0123456789 a_0123456789 FalseSym0)
                                                  lambda = n
                                                in lambda } ::
                                           Sing (Case_0123456789 n b a_0123456789 a_0123456789 (Let0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789))
                               in lambda sN sB)))
                   a_0123456789)
                a_0123456789
        in lambda sA_0123456789 sA_0123456789
    sLiftMaybe sF (SJust sX)
      = let
          lambda ::
            forall f x. (t ~ f, t ~ Apply JustSym0 x) =>
            Sing f
            -> Sing x
               -> Sing (Apply (Apply LiftMaybeSym0 f) (Apply JustSym0 x) :: Maybe b)
          lambda f x
            = applySing
                (singFun1 (Proxy :: Proxy JustSym0) SJust) (applySing f x)
        in lambda sF sX
    sLiftMaybe _s_z_0123456789 SNothing
      = let
          lambda ::
            forall _z_0123456789. (t ~ _z_0123456789, t ~ NothingSym0) =>
            Sing _z_0123456789
            -> Sing (Apply (Apply LiftMaybeSym0 _z_0123456789) NothingSym0 :: Maybe b)
          lambda _z_0123456789 = SNothing
        in lambda _s_z_0123456789
    sMap _s_z_0123456789 SNil
      = let
          lambda ::
            forall _z_0123456789. (t ~ _z_0123456789, t ~ '[]) =>
            Sing _z_0123456789
            -> Sing (Apply (Apply MapSym0 _z_0123456789) '[] :: [b])
          lambda _z_0123456789 = SNil
        in lambda _s_z_0123456789
    sMap sF (SCons sH sT)
      = let
          lambda ::
            forall f h t. (t ~ f, t ~ Apply (Apply (:$) h) t) =>
            Sing f
            -> Sing h
               -> Sing t
                  -> Sing (Apply (Apply MapSym0 f) (Apply (Apply (:$) h) t) :: [b])
          lambda f h t
            = applySing
                (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) (applySing f h))
                (applySing
                   (applySing (singFun2 (Proxy :: Proxy MapSym0) sMap) f) t)
        in lambda sF sH sT
    data instance Sing (z :: Either a b)
      = forall (n :: a). z ~ Left n => SLeft (Sing (n :: a)) |
        forall (n :: b). z ~ Right n => SRight (Sing (n :: b))
    type SEither = (Sing :: Either a b -> *)
    instance (SingKind (KProxy :: KProxy a),
              SingKind (KProxy :: KProxy b)) =>
             SingKind (KProxy :: KProxy (Either a b)) where
      type DemoteRep (KProxy :: KProxy (Either a b)) = Either (DemoteRep (KProxy :: KProxy a)) (DemoteRep (KProxy :: KProxy b))
      fromSing (SLeft b) = Left (fromSing b)
      fromSing (SRight b) = Right (fromSing b)
      toSing (Left b)
        = case toSing b :: SomeSing (KProxy :: KProxy a) of {
            SomeSing c -> SomeSing (SLeft c) }
      toSing (Right b)
        = case toSing b :: SomeSing (KProxy :: KProxy b) of {
            SomeSing c -> SomeSing (SRight c) }
    instance SingI n => SingI (Left (n :: a)) where
      sing = SLeft sing
    instance SingI n => SingI (Right (n :: b)) where
      sing = SRight sing