singletons-base-3.2: tests/compile-and-dump/Singletons/Classes2.golden
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