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 = ZeroFoo type SuccFooSym1 (t :: NatFoo) = SuccFoo t instance SuppressUnusedWarnings SuccFooSym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) SuccFooSym0KindInference) GHC.Tuple.()) data SuccFooSym0 (l :: TyFun NatFoo NatFoo) = forall arg. SameKind (Apply SuccFooSym0 arg) (SuccFooSym1 arg) => SuccFooSym0KindInference type instance Apply SuccFooSym0 l = SuccFoo l 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_0123456789876543210Sym2 (t :: NatFoo) (t :: NatFoo) = Mycompare_0123456789876543210 t t instance SuppressUnusedWarnings Mycompare_0123456789876543210Sym1 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) Mycompare_0123456789876543210Sym1KindInference) GHC.Tuple.()) data Mycompare_0123456789876543210Sym1 (l :: NatFoo) (l :: TyFun NatFoo Ordering) = forall arg. SameKind (Apply (Mycompare_0123456789876543210Sym1 l) arg) (Mycompare_0123456789876543210Sym2 l arg) => Mycompare_0123456789876543210Sym1KindInference type instance Apply (Mycompare_0123456789876543210Sym1 l) l = Mycompare_0123456789876543210 l l instance SuppressUnusedWarnings Mycompare_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) Mycompare_0123456789876543210Sym0KindInference) GHC.Tuple.()) data Mycompare_0123456789876543210Sym0 (l :: TyFun NatFoo (TyFun NatFoo Ordering -> GHC.Types.Type)) = forall arg. SameKind (Apply Mycompare_0123456789876543210Sym0 arg) (Mycompare_0123456789876543210Sym1 arg) => Mycompare_0123456789876543210Sym0KindInference type instance Apply Mycompare_0123456789876543210Sym0 l = Mycompare_0123456789876543210Sym1 l instance PMyOrd NatFoo where type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a data instance Sing (z :: NatFoo) where SZeroFoo :: Sing ZeroFoo SSuccFoo :: forall (n :: NatFoo). (Sing (n :: NatFoo)) -> Sing (SuccFoo n) type SNatFoo = (Sing :: NatFoo -> GHC.Types.Type) 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 (TyFun NatFoo Ordering -> GHC.Types.Type) -> GHC.Types.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