singletons-base-3.1: tests/compile-and-dump/Promote/GenDefunSymbols.golden
Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
genDefunSymbols [''LiftMaybe, ''NatT, ''(:+)]
======>
type LiftMaybeSym0 :: forall (a :: Type)
(b :: Type). (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
data LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
where
LiftMaybeSym0KindInference :: Data.Singletons.SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
LiftMaybeSym0 a0123456789876543210
type instance Apply LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings LiftMaybeSym0 where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) LiftMaybeSym0KindInference) ())
type LiftMaybeSym1 :: forall (a :: Type) (b :: Type). (~>) a b
-> (~>) (Maybe a) (Maybe b)
data LiftMaybeSym1 (a0123456789876543210 :: (~>) a b) :: (~>) (Maybe a) (Maybe b)
where
LiftMaybeSym1KindInference :: Data.Singletons.SameKind (Apply (LiftMaybeSym1 a0123456789876543210) arg) (LiftMaybeSym2 a0123456789876543210 arg) =>
LiftMaybeSym1 a0123456789876543210 a0123456789876543210
type instance Apply (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) LiftMaybeSym1KindInference) ())
type LiftMaybeSym2 :: forall (a :: Type) (b :: Type). (~>) a b
-> Maybe a -> Maybe b
type family LiftMaybeSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where
LiftMaybeSym2 a0123456789876543210 a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
type ZeroSym0 :: NatT
type family ZeroSym0 :: NatT where
ZeroSym0 = 'Zero
type SuccSym0 :: (~>) NatT NatT
data SuccSym0 :: (~>) NatT NatT
where
SuccSym0KindInference :: Data.Singletons.SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0 a0123456789876543210
type instance Apply SuccSym0 a0123456789876543210 = 'Succ a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings SuccSym0 where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) SuccSym0KindInference) ())
type SuccSym1 :: NatT -> NatT
type family SuccSym1 (a0123456789876543210 :: NatT) :: NatT where
SuccSym1 a0123456789876543210 = 'Succ a0123456789876543210
type (:+@#@$) :: (~>) Natural ((~>) Natural Natural)
data (:+@#@$) :: (~>) Natural ((~>) Natural Natural)
where
(::+@#@$###) :: Data.Singletons.SameKind (Apply (:+@#@$) arg) ((:+@#@$$) arg) =>
(:+@#@$) a0123456789876543210
type instance Apply (:+@#@$) a0123456789876543210 = (:+@#@$$) a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings (:+@#@$) where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) (::+@#@$###)) ())
type (:+@#@$$) :: Natural -> (~>) Natural Natural
data (:+@#@$$) (a0123456789876543210 :: Natural) :: (~>) Natural Natural
where
(::+@#@$$###) :: Data.Singletons.SameKind (Apply ((:+@#@$$) a0123456789876543210) arg) ((:+@#@$$$) a0123456789876543210 arg) =>
(:+@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:+@#@$$) a0123456789876543210) a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings ((:+@#@$$) a0123456789876543210) where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) (::+@#@$$###)) ())
type (:+@#@$$$) :: Natural -> Natural -> Natural
type family (:+@#@$$$) (a0123456789876543210 :: Natural) (a0123456789876543210 :: Natural) :: Natural where
(:+@#@$$$) a0123456789876543210 a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210