Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| data Nat
            = Zero | Succ Nat
            deriving (Eq, Ord)
          data Foo a b c d
            = A a b c d |
              B a b c d |
              C a b c d |
              D a b c d |
              E a b c d |
              F a b c d
            deriving (Eq, Ord) |]
  ======>
    data Nat
      = Zero | Succ Nat
      deriving (Eq, Ord)
    data Foo a b c d
      = A a b c d |
        B a b c d |
        C a b c d |
        D a b c d |
        E a b c d |
        F a b c d
      deriving (Eq, Ord)
    type ZeroSym0 = Zero
    type SuccSym1 (t :: Nat) = Succ t
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
    data SuccSym0 (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = Succ l
    type ASym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        A t t t t
    instance SuppressUnusedWarnings ASym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ASym3KindInference) GHC.Tuple.())
    data ASym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (ASym3 l l l) arg) (ASym4 l l l arg) =>
        ASym3KindInference
    type instance Apply (ASym3 l l l) l = A l l l l
    instance SuppressUnusedWarnings ASym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ASym2KindInference) GHC.Tuple.())
    data ASym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ASym2 l l) arg) (ASym3 l l arg) =>
        ASym2KindInference
    type instance Apply (ASym2 l l) l = ASym3 l l l
    instance SuppressUnusedWarnings ASym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ASym1KindInference) GHC.Tuple.())
    data ASym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ASym1 l) arg) (ASym2 l arg) =>
        ASym1KindInference
    type instance Apply (ASym1 l) l = ASym2 l l
    instance SuppressUnusedWarnings ASym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ASym0KindInference) GHC.Tuple.())
    data ASym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply ASym0 arg) (ASym1 arg) =>
        ASym0KindInference
    type instance Apply ASym0 l = ASym1 l
    type BSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        B t t t t
    instance SuppressUnusedWarnings BSym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BSym3KindInference) GHC.Tuple.())
    data BSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (BSym3 l l l) arg) (BSym4 l l l arg) =>
        BSym3KindInference
    type instance Apply (BSym3 l l l) l = B l l l l
    instance SuppressUnusedWarnings BSym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BSym2KindInference) GHC.Tuple.())
    data BSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (BSym2 l l) arg) (BSym3 l l arg) =>
        BSym2KindInference
    type instance Apply (BSym2 l l) l = BSym3 l l l
    instance SuppressUnusedWarnings BSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BSym1KindInference) GHC.Tuple.())
    data BSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (BSym1 l) arg) (BSym2 l arg) =>
        BSym1KindInference
    type instance Apply (BSym1 l) l = BSym2 l l
    instance SuppressUnusedWarnings BSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BSym0KindInference) GHC.Tuple.())
    data BSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply BSym0 arg) (BSym1 arg) =>
        BSym0KindInference
    type instance Apply BSym0 l = BSym1 l
    type CSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        C t t t t
    instance SuppressUnusedWarnings CSym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) CSym3KindInference) GHC.Tuple.())
    data CSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (CSym3 l l l) arg) (CSym4 l l l arg) =>
        CSym3KindInference
    type instance Apply (CSym3 l l l) l = C l l l l
    instance SuppressUnusedWarnings CSym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) CSym2KindInference) GHC.Tuple.())
    data CSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (CSym2 l l) arg) (CSym3 l l arg) =>
        CSym2KindInference
    type instance Apply (CSym2 l l) l = CSym3 l l l
    instance SuppressUnusedWarnings CSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) CSym1KindInference) GHC.Tuple.())
    data CSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (CSym1 l) arg) (CSym2 l arg) =>
        CSym1KindInference
    type instance Apply (CSym1 l) l = CSym2 l l
    instance SuppressUnusedWarnings CSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) CSym0KindInference) GHC.Tuple.())
    data CSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply CSym0 arg) (CSym1 arg) =>
        CSym0KindInference
    type instance Apply CSym0 l = CSym1 l
    type DSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        D t t t t
    instance SuppressUnusedWarnings DSym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) DSym3KindInference) GHC.Tuple.())
    data DSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (DSym3 l l l) arg) (DSym4 l l l arg) =>
        DSym3KindInference
    type instance Apply (DSym3 l l l) l = D l l l l
    instance SuppressUnusedWarnings DSym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) DSym2KindInference) GHC.Tuple.())
    data DSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (DSym2 l l) arg) (DSym3 l l arg) =>
        DSym2KindInference
    type instance Apply (DSym2 l l) l = DSym3 l l l
    instance SuppressUnusedWarnings DSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) DSym1KindInference) GHC.Tuple.())
    data DSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (DSym1 l) arg) (DSym2 l arg) =>
        DSym1KindInference
    type instance Apply (DSym1 l) l = DSym2 l l
    instance SuppressUnusedWarnings DSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) DSym0KindInference) GHC.Tuple.())
    data DSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply DSym0 arg) (DSym1 arg) =>
        DSym0KindInference
    type instance Apply DSym0 l = DSym1 l
    type ESym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        E t t t t
    instance SuppressUnusedWarnings ESym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ESym3KindInference) GHC.Tuple.())
    data ESym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (ESym3 l l l) arg) (ESym4 l l l arg) =>
        ESym3KindInference
    type instance Apply (ESym3 l l l) l = E l l l l
    instance SuppressUnusedWarnings ESym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ESym2KindInference) GHC.Tuple.())
    data ESym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ESym2 l l) arg) (ESym3 l l arg) =>
        ESym2KindInference
    type instance Apply (ESym2 l l) l = ESym3 l l l
    instance SuppressUnusedWarnings ESym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ESym1KindInference) GHC.Tuple.())
    data ESym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ESym1 l) arg) (ESym2 l arg) =>
        ESym1KindInference
    type instance Apply (ESym1 l) l = ESym2 l l
    instance SuppressUnusedWarnings ESym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ESym0KindInference) GHC.Tuple.())
    data ESym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply ESym0 arg) (ESym1 arg) =>
        ESym0KindInference
    type instance Apply ESym0 l = ESym1 l
    type FSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
        F t t t t
    instance SuppressUnusedWarnings FSym3 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) FSym3KindInference) GHC.Tuple.())
    data FSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
      = forall arg. SameKind (Apply (FSym3 l l l) arg) (FSym4 l l l arg) =>
        FSym3KindInference
    type instance Apply (FSym3 l l l) l = F l l l l
    instance SuppressUnusedWarnings FSym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) FSym2KindInference) GHC.Tuple.())
    data FSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply (FSym2 l l) arg) (FSym3 l l arg) =>
        FSym2KindInference
    type instance Apply (FSym2 l l) l = FSym3 l l l
    instance SuppressUnusedWarnings FSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) FSym1KindInference) GHC.Tuple.())
    data FSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (FSym1 l) arg) (FSym2 l arg) =>
        FSym1KindInference
    type instance Apply (FSym1 l) l = FSym2 l l
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) FSym0KindInference) GHC.Tuple.())
    data FSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
                                                                                                         -> GHC.Types.Type)
                                                                             -> GHC.Types.Type)
                                                 -> GHC.Types.Type))
      = forall arg. SameKind (Apply FSym0 arg) (FSym1 arg) =>
        FSym0KindInference
    type instance Apply FSym0 l = FSym1 l
    type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
      Compare_0123456789876543210 Zero (Succ _) = LTSym0
      Compare_0123456789876543210 (Succ _) Zero = GTSym0
    type Compare_0123456789876543210Sym2 (t :: Nat) (t :: Nat) =
        Compare_0123456789876543210 t t
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym1 (l :: Nat) (l :: TyFun Nat Ordering)
      = forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
        Compare_0123456789876543210Sym1KindInference
    type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym0 (l :: TyFun Nat (TyFun Nat Ordering
                                                          -> GHC.Types.Type))
      = forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
        Compare_0123456789876543210Sym0KindInference
    type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
    instance POrd Nat where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type family Compare_0123456789876543210 (a :: Foo a b c d) (a :: Foo a b c d) :: Ordering where
      Compare_0123456789876543210 (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (D a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (D b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (E a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (E b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (F a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (F b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]))))
      Compare_0123456789876543210 (A _ _ _ _) (B _ _ _ _) = LTSym0
      Compare_0123456789876543210 (A _ _ _ _) (C _ _ _ _) = LTSym0
      Compare_0123456789876543210 (A _ _ _ _) (D _ _ _ _) = LTSym0
      Compare_0123456789876543210 (A _ _ _ _) (E _ _ _ _) = LTSym0
      Compare_0123456789876543210 (A _ _ _ _) (F _ _ _ _) = LTSym0
      Compare_0123456789876543210 (B _ _ _ _) (A _ _ _ _) = GTSym0
      Compare_0123456789876543210 (B _ _ _ _) (C _ _ _ _) = LTSym0
      Compare_0123456789876543210 (B _ _ _ _) (D _ _ _ _) = LTSym0
      Compare_0123456789876543210 (B _ _ _ _) (E _ _ _ _) = LTSym0
      Compare_0123456789876543210 (B _ _ _ _) (F _ _ _ _) = LTSym0
      Compare_0123456789876543210 (C _ _ _ _) (A _ _ _ _) = GTSym0
      Compare_0123456789876543210 (C _ _ _ _) (B _ _ _ _) = GTSym0
      Compare_0123456789876543210 (C _ _ _ _) (D _ _ _ _) = LTSym0
      Compare_0123456789876543210 (C _ _ _ _) (E _ _ _ _) = LTSym0
      Compare_0123456789876543210 (C _ _ _ _) (F _ _ _ _) = LTSym0
      Compare_0123456789876543210 (D _ _ _ _) (A _ _ _ _) = GTSym0
      Compare_0123456789876543210 (D _ _ _ _) (B _ _ _ _) = GTSym0
      Compare_0123456789876543210 (D _ _ _ _) (C _ _ _ _) = GTSym0
      Compare_0123456789876543210 (D _ _ _ _) (E _ _ _ _) = LTSym0
      Compare_0123456789876543210 (D _ _ _ _) (F _ _ _ _) = LTSym0
      Compare_0123456789876543210 (E _ _ _ _) (A _ _ _ _) = GTSym0
      Compare_0123456789876543210 (E _ _ _ _) (B _ _ _ _) = GTSym0
      Compare_0123456789876543210 (E _ _ _ _) (C _ _ _ _) = GTSym0
      Compare_0123456789876543210 (E _ _ _ _) (D _ _ _ _) = GTSym0
      Compare_0123456789876543210 (E _ _ _ _) (F _ _ _ _) = LTSym0
      Compare_0123456789876543210 (F _ _ _ _) (A _ _ _ _) = GTSym0
      Compare_0123456789876543210 (F _ _ _ _) (B _ _ _ _) = GTSym0
      Compare_0123456789876543210 (F _ _ _ _) (C _ _ _ _) = GTSym0
      Compare_0123456789876543210 (F _ _ _ _) (D _ _ _ _) = GTSym0
      Compare_0123456789876543210 (F _ _ _ _) (E _ _ _ _) = GTSym0
    type Compare_0123456789876543210Sym2 (t :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (t :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) =
        Compare_0123456789876543210 t t
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym1 (l :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (l :: TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering)
      = forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
        Compare_0123456789876543210Sym1KindInference
    type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym0 (l :: TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering
                                                                                                                                                -> GHC.Types.Type))
      = forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
        Compare_0123456789876543210Sym0KindInference
    type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
    instance POrd (Foo a b c d) where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789876543210 Zero Zero = TrueSym0
      Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b
      Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0
    instance PEq Nat where
      type (==) a b = Equals_0123456789876543210 a b
    type family Equals_0123456789876543210 (a :: Foo a b c d) (b :: Foo a b c d) :: Bool where
      Equals_0123456789876543210 (A a a a a) (A b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (B a a a a) (B b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (C a a a a) (C b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (D a a a a) (D b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (E a a a a) (E b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (F a a a a) (F b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b)))
      Equals_0123456789876543210 (_ :: Foo a b c d) (_ :: Foo a b c d) = FalseSym0
    instance PEq (Foo a b c d) where
      type (==) a b = Equals_0123456789876543210 a b
    data instance Sing (z :: Nat)
      where
        SZero :: Sing Zero
        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n)
    type SNat = (Sing :: Nat -> GHC.Types.Type)
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ (b :: Demote Nat))
        = case toSing b :: SomeSing Nat of {
            SomeSing c -> SomeSing (SSucc c) }
    data instance Sing (z :: Foo a b c d)
      where
        SA :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (A n n n n)
        SB :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (B n n n n)
        SC :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (C n n n n)
        SD :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (D n n n n)
        SE :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (E n n n n)
        SF :: forall (n :: a) (n :: b) (n :: c) (n :: d).
              (Sing (n :: a))
              -> (Sing (n :: b))
                 -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (F n n n n)
    type SFoo = (Sing :: Foo a b c d -> GHC.Types.Type)
    instance (SingKind a, SingKind b, SingKind c, SingKind d) =>
             SingKind (Foo a b c d) where
      type Demote (Foo a b c d) = Foo (Demote a) (Demote b) (Demote c) (Demote d)
      fromSing (SA b b b b)
        = (((A (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      fromSing (SB b b b b)
        = (((B (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      fromSing (SC b b b b)
        = (((C (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      fromSing (SD b b b b)
        = (((D (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      fromSing (SE b b b b)
        = (((E (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      fromSing (SF b b b b)
        = (((F (fromSing b)) (fromSing b)) (fromSing b)) (fromSing b)
      toSing
        (A (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SA c) c) c) c) }
      toSing
        (B (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SB c) c) c) c) }
      toSing
        (C (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SC c) c) c) c) }
      toSing
        (D (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SD c) c) c) c) }
      toSing
        (E (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SE c) c) c) c) }
      toSing
        (F (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
        = case
              (((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
                  (toSing b :: SomeSing b))
                 (toSing b :: SomeSing c))
                (toSing b :: SomeSing d)
          of {
            GHC.Tuple.(,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing ((((SF c) c) c) c) }
    instance SOrd Nat => SOrd Nat where
      sCompare ::
        forall (t1 :: Nat) (t2 :: Nat).
        Sing t1
        -> Sing t2
           -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat (TyFun Nat Ordering
                                                            -> GHC.Types.Type)
                                                 -> GHC.Types.Type) t1) t2)
      sCompare SZero SZero
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            SNil
      sCompare
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               SNil)
      sCompare SZero (SSucc _) = SLT
      sCompare (SSucc _) SZero = SGT
    instance (SOrd a, SOrd b, SOrd c, SOrd d) =>
             SOrd (Foo a b c d) where
      sCompare ::
        forall (t1 :: Foo a b c d) (t2 :: Foo a b c d).
        Sing t1
        -> Sing t2
           -> Sing (Apply (Apply (CompareSym0 :: TyFun (Foo a b c d) (TyFun (Foo a b c d) Ordering
                                                                      -> GHC.Types.Type)
                                                 -> GHC.Types.Type) t1) t2)
      sCompare
        (SA (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SA (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare
        (SB (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SB (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare
        (SC (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SC (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare
        (SD (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SD (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare
        (SE (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SE (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare
        (SF (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210)
            (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SF (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210)
            (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               ((applySing
                   ((applySing ((singFun2 @(:@#@$)) SCons))
                      ((applySing
                          ((applySing ((singFun2 @CompareSym0) sCompare))
                             sA_0123456789876543210))
                         sB_0123456789876543210)))
                  ((applySing
                      ((applySing ((singFun2 @(:@#@$)) SCons))
                         ((applySing
                             ((applySing ((singFun2 @CompareSym0) sCompare))
                                sA_0123456789876543210))
                            sB_0123456789876543210)))
                     ((applySing
                         ((applySing ((singFun2 @(:@#@$)) SCons))
                            ((applySing
                                ((applySing ((singFun2 @CompareSym0) sCompare))
                                   sA_0123456789876543210))
                               sB_0123456789876543210)))
                        SNil))))
      sCompare (SA _ _ _ _) (SB _ _ _ _) = SLT
      sCompare (SA _ _ _ _) (SC _ _ _ _) = SLT
      sCompare (SA _ _ _ _) (SD _ _ _ _) = SLT
      sCompare (SA _ _ _ _) (SE _ _ _ _) = SLT
      sCompare (SA _ _ _ _) (SF _ _ _ _) = SLT
      sCompare (SB _ _ _ _) (SA _ _ _ _) = SGT
      sCompare (SB _ _ _ _) (SC _ _ _ _) = SLT
      sCompare (SB _ _ _ _) (SD _ _ _ _) = SLT
      sCompare (SB _ _ _ _) (SE _ _ _ _) = SLT
      sCompare (SB _ _ _ _) (SF _ _ _ _) = SLT
      sCompare (SC _ _ _ _) (SA _ _ _ _) = SGT
      sCompare (SC _ _ _ _) (SB _ _ _ _) = SGT
      sCompare (SC _ _ _ _) (SD _ _ _ _) = SLT
      sCompare (SC _ _ _ _) (SE _ _ _ _) = SLT
      sCompare (SC _ _ _ _) (SF _ _ _ _) = SLT
      sCompare (SD _ _ _ _) (SA _ _ _ _) = SGT
      sCompare (SD _ _ _ _) (SB _ _ _ _) = SGT
      sCompare (SD _ _ _ _) (SC _ _ _ _) = SGT
      sCompare (SD _ _ _ _) (SE _ _ _ _) = SLT
      sCompare (SD _ _ _ _) (SF _ _ _ _) = SLT
      sCompare (SE _ _ _ _) (SA _ _ _ _) = SGT
      sCompare (SE _ _ _ _) (SB _ _ _ _) = SGT
      sCompare (SE _ _ _ _) (SC _ _ _ _) = SGT
      sCompare (SE _ _ _ _) (SD _ _ _ _) = SGT
      sCompare (SE _ _ _ _) (SF _ _ _ _) = SLT
      sCompare (SF _ _ _ _) (SA _ _ _ _) = SGT
      sCompare (SF _ _ _ _) (SB _ _ _ _) = SGT
      sCompare (SF _ _ _ _) (SC _ _ _ _) = SGT
      sCompare (SF _ _ _ _) (SD _ _ _ _) = SGT
      sCompare (SF _ _ _ _) (SE _ _ _ _) = SGT
    instance SEq Nat => SEq Nat where
      (%==) SZero SZero = STrue
      (%==) SZero (SSucc _) = SFalse
      (%==) (SSucc _) SZero = SFalse
      (%==) (SSucc a) (SSucc b) = ((%==) a) b
    instance SDecide Nat => SDecide Nat where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _) = Disproved (\ x -> case x of)
      (%~) (SSucc _) SZero = Disproved (\ x -> case x of)
      (%~) (SSucc a) (SSucc b)
        = case ((%~) a) b of
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
    instance (SEq a, SEq b, SEq c, SEq d) => SEq (Foo a b c d) where
      (%==) (SA a a a a) (SA b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
      (%==) (SA _ _ _ _) (SB _ _ _ _) = SFalse
      (%==) (SA _ _ _ _) (SC _ _ _ _) = SFalse
      (%==) (SA _ _ _ _) (SD _ _ _ _) = SFalse
      (%==) (SA _ _ _ _) (SE _ _ _ _) = SFalse
      (%==) (SA _ _ _ _) (SF _ _ _ _) = SFalse
      (%==) (SB _ _ _ _) (SA _ _ _ _) = SFalse
      (%==) (SB a a a a) (SB b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
      (%==) (SB _ _ _ _) (SC _ _ _ _) = SFalse
      (%==) (SB _ _ _ _) (SD _ _ _ _) = SFalse
      (%==) (SB _ _ _ _) (SE _ _ _ _) = SFalse
      (%==) (SB _ _ _ _) (SF _ _ _ _) = SFalse
      (%==) (SC _ _ _ _) (SA _ _ _ _) = SFalse
      (%==) (SC _ _ _ _) (SB _ _ _ _) = SFalse
      (%==) (SC a a a a) (SC b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
      (%==) (SC _ _ _ _) (SD _ _ _ _) = SFalse
      (%==) (SC _ _ _ _) (SE _ _ _ _) = SFalse
      (%==) (SC _ _ _ _) (SF _ _ _ _) = SFalse
      (%==) (SD _ _ _ _) (SA _ _ _ _) = SFalse
      (%==) (SD _ _ _ _) (SB _ _ _ _) = SFalse
      (%==) (SD _ _ _ _) (SC _ _ _ _) = SFalse
      (%==) (SD a a a a) (SD b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
      (%==) (SD _ _ _ _) (SE _ _ _ _) = SFalse
      (%==) (SD _ _ _ _) (SF _ _ _ _) = SFalse
      (%==) (SE _ _ _ _) (SA _ _ _ _) = SFalse
      (%==) (SE _ _ _ _) (SB _ _ _ _) = SFalse
      (%==) (SE _ _ _ _) (SC _ _ _ _) = SFalse
      (%==) (SE _ _ _ _) (SD _ _ _ _) = SFalse
      (%==) (SE a a a a) (SE b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
      (%==) (SE _ _ _ _) (SF _ _ _ _) = SFalse
      (%==) (SF _ _ _ _) (SA _ _ _ _) = SFalse
      (%==) (SF _ _ _ _) (SB _ _ _ _) = SFalse
      (%==) (SF _ _ _ _) (SC _ _ _ _) = SFalse
      (%==) (SF _ _ _ _) (SD _ _ _ _) = SFalse
      (%==) (SF _ _ _ _) (SE _ _ _ _) = SFalse
      (%==) (SF a a a a) (SF b b b b)
        = ((%&&) (((%==) a) b))
            (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b)))
    instance (SDecide a, SDecide b, SDecide c, SDecide d) =>
             SDecide (Foo a b c d) where
      (%~) (SA a a a a) (SA b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
      (%~) (SA _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SA _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SA _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SA _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SA _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SB _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SB a a a a) (SB b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
      (%~) (SB _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SB _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SB _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SB _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SC _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SC _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SC a a a a) (SC b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
      (%~) (SC _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SC _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SC _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SD _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SD _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SD _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SD a a a a) (SD b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
      (%~) (SD _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SD _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SE _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SE _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SE _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SE _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SE a a a a) (SE b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
      (%~) (SE _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of)
      (%~) (SF a a a a) (SF b b b b)
        = case
              (((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
                (((%~) a) b)
          of
            GHC.Tuple.(,,,) (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
                            (Proved Refl)
              -> Proved Refl
            GHC.Tuple.(,,,) (Disproved contra) _ _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ (Disproved contra) _ _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            GHC.Tuple.(,,,) _ _ _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (A (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SA sing) sing) sing) sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (B (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SB sing) sing) sing) sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (C (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SC sing) sing) sing) sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (D (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SD sing) sing) sing) sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (E (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SE sing) sing) sing) sing
    instance (SingI n, SingI n, SingI n, SingI n) =>
             SingI (F (n :: a) (n :: b) (n :: c) (n :: d)) where
      sing = (((SF sing) sing) sing) sing