Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| data NatFoo = ZeroFoo | SuccFoo NatFoo
          
          instance MyOrd NatFoo where
            ZeroFoo `mycompare` ZeroFoo = EQ
            ZeroFoo `mycompare` (SuccFoo _) = LT
            (SuccFoo _) `mycompare` ZeroFoo = GT
            (SuccFoo n) `mycompare` (SuccFoo m) = m `mycompare` n |]
  ======>
    data NatFoo = ZeroFoo | SuccFoo NatFoo
    instance MyOrd NatFoo where
      mycompare ZeroFoo ZeroFoo = EQ
      mycompare ZeroFoo (SuccFoo _) = LT
      mycompare (SuccFoo _) ZeroFoo = GT
      mycompare (SuccFoo n) (SuccFoo m) = (m `mycompare` n)
    type ZeroFooSym0 :: NatFoo
    type family ZeroFooSym0 :: NatFoo where
      ZeroFooSym0 = ZeroFoo
    type SuccFooSym0 :: (~>) NatFoo NatFoo
    data SuccFooSym0 :: (~>) NatFoo NatFoo
      where
        SuccFooSym0KindInference :: SameKind (Apply SuccFooSym0 arg) (SuccFooSym1 arg) =>
                                    SuccFooSym0 a0123456789876543210
    type instance Apply SuccFooSym0 a0123456789876543210 = SuccFoo a0123456789876543210
    instance SuppressUnusedWarnings SuccFooSym0 where
      suppressUnusedWarnings = snd ((,) SuccFooSym0KindInference ())
    type SuccFooSym1 :: NatFoo -> NatFoo
    type family SuccFooSym1 (a0123456789876543210 :: NatFoo) :: NatFoo where
      SuccFooSym1 a0123456789876543210 = SuccFoo a0123456789876543210
    type Mycompare_0123456789876543210 :: NatFoo -> NatFoo -> Ordering
    type family Mycompare_0123456789876543210 (a :: NatFoo) (a :: NatFoo) :: Ordering where
      Mycompare_0123456789876543210 ZeroFoo ZeroFoo = EQSym0
      Mycompare_0123456789876543210 ZeroFoo (SuccFoo _) = LTSym0
      Mycompare_0123456789876543210 (SuccFoo _) ZeroFoo = GTSym0
      Mycompare_0123456789876543210 (SuccFoo n) (SuccFoo m) = Apply (Apply MycompareSym0 m) n
    type Mycompare_0123456789876543210Sym0 :: (~>) NatFoo ((~>) NatFoo Ordering)
    data Mycompare_0123456789876543210Sym0 :: (~>) NatFoo ((~>) NatFoo Ordering)
      where
        Mycompare_0123456789876543210Sym0KindInference :: SameKind (Apply Mycompare_0123456789876543210Sym0 arg) (Mycompare_0123456789876543210Sym1 arg) =>
                                                          Mycompare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Mycompare_0123456789876543210Sym0 a0123456789876543210 = Mycompare_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings Mycompare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Mycompare_0123456789876543210Sym0KindInference ())
    type Mycompare_0123456789876543210Sym1 :: NatFoo
                                              -> (~>) NatFoo Ordering
    data Mycompare_0123456789876543210Sym1 (a0123456789876543210 :: NatFoo) :: (~>) NatFoo Ordering
      where
        Mycompare_0123456789876543210Sym1KindInference :: SameKind (Apply (Mycompare_0123456789876543210Sym1 a0123456789876543210) arg) (Mycompare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          Mycompare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (Mycompare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Mycompare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Mycompare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Mycompare_0123456789876543210Sym1KindInference ())
    type Mycompare_0123456789876543210Sym2 :: NatFoo
                                              -> NatFoo -> Ordering
    type family Mycompare_0123456789876543210Sym2 (a0123456789876543210 :: NatFoo) (a0123456789876543210 :: NatFoo) :: Ordering where
      Mycompare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Mycompare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PMyOrd NatFoo where
      type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a
    data SNatFoo :: NatFoo -> Type
      where
        SZeroFoo :: SNatFoo (ZeroFoo :: NatFoo)
        SSuccFoo :: forall (n :: NatFoo).
                    (Sing n) -> SNatFoo (SuccFoo n :: NatFoo)
    type instance Sing @NatFoo = SNatFoo
    instance SingKind NatFoo where
      type Demote NatFoo = NatFoo
      fromSing SZeroFoo = ZeroFoo
      fromSing (SSuccFoo b) = SuccFoo (fromSing b)
      toSing ZeroFoo = SomeSing SZeroFoo
      toSing (SuccFoo (b :: Demote NatFoo))
        = case toSing b :: SomeSing NatFoo of
            SomeSing c -> SomeSing (SSuccFoo c)
    instance SMyOrd NatFoo where
      sMycompare ::
        forall (t1 :: NatFoo) (t2 :: NatFoo). Sing t1
                                              -> Sing t2
                                                 -> Sing (Apply (Apply (MycompareSym0 :: TyFun NatFoo ((~>) NatFoo Ordering)
                                                                                         -> Type) t1) t2)
      sMycompare SZeroFoo SZeroFoo = SEQ
      sMycompare SZeroFoo (SSuccFoo _) = SLT
      sMycompare (SSuccFoo _) SZeroFoo = SGT
      sMycompare (SSuccFoo (sN :: Sing n)) (SSuccFoo (sM :: Sing m))
        = applySing (applySing (singFun2 @MycompareSym0 sMycompare) sM) sN
    instance SingI ZeroFoo where
      sing = SZeroFoo
    instance SingI n => SingI (SuccFoo (n :: NatFoo)) where
      sing = SSuccFoo sing
    instance SingI1 SuccFoo where
      liftSing = SSuccFoo
    instance SingI (SuccFooSym0 :: (~>) NatFoo NatFoo) where
      sing = singFun1 @SuccFooSym0 SSuccFoo