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 (t0123456789876543210 :: NatFoo) = SuccFoo t0123456789876543210 instance SuppressUnusedWarnings SuccFooSym0 where suppressUnusedWarnings = snd (((,) SuccFooSym0KindInference) ()) data SuccFooSym0 :: (~>) NatFoo NatFoo where SuccFooSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply SuccFooSym0 arg) (SuccFooSym1 arg) => SuccFooSym0 t0123456789876543210 type instance Apply SuccFooSym0 t0123456789876543210 = SuccFoo t0123456789876543210 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 (a0123456789876543210 :: NatFoo) (a0123456789876543210 :: NatFoo) = Mycompare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Mycompare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Mycompare_0123456789876543210Sym1KindInference) ()) data Mycompare_0123456789876543210Sym1 (a0123456789876543210 :: NatFoo) :: (~>) NatFoo Ordering where Mycompare_0123456789876543210Sym1KindInference :: forall a0123456789876543210 a0123456789876543210 arg. 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_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Mycompare_0123456789876543210Sym0KindInference) ()) data Mycompare_0123456789876543210Sym0 :: (~>) NatFoo ((~>) NatFoo Ordering) where Mycompare_0123456789876543210Sym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply Mycompare_0123456789876543210Sym0 arg) (Mycompare_0123456789876543210Sym1 arg) => Mycompare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Mycompare_0123456789876543210Sym0 a0123456789876543210 = Mycompare_0123456789876543210Sym1 a0123456789876543210 instance PMyOrd NatFoo where type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a data instance Sing :: NatFoo -> GHC.Types.Type 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 ((~>) NatFoo Ordering) -> 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 instance SingI (SuccFooSym0 :: (~>) NatFoo NatFoo) where sing = (singFun1 @SuccFooSym0) SSuccFoo instance SingI (TyCon1 SuccFoo :: (~>) NatFoo NatFoo) where sing = (singFun1 @(TyCon1 SuccFoo)) SSuccFoo