singletons-2.5: tests/compile-and-dump/Singletons/HigherOrder.ghc86.template
Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (h : t) = (f h) : (map f t)
liftMaybe :: (a -> b) -> Maybe a -> Maybe b
liftMaybe f (Just x) = Just (f x)
liftMaybe _ Nothing = Nothing
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (x : xs) (y : ys) = f x y : zipWith f xs ys
zipWith _ [] [] = []
zipWith _ (_ : _) [] = []
zipWith _ [] (_ : _) = []
foo :: ((a -> b) -> a -> b) -> (a -> b) -> a -> b
foo f g a = f g a
splunge :: [Nat] -> [Bool] -> [Nat]
splunge ns bs
= zipWith (\ n b -> if b then Succ (Succ n) else n) ns bs
etad :: [Nat] -> [Bool] -> [Nat]
etad = zipWith (\ n b -> if b then Succ (Succ n) else n)
data Either a b = Left a | Right b |]
======>
data Either a b = Left a | Right b
map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (h : t) = (f h : (map f) t)
liftMaybe :: (a -> b) -> Maybe a -> Maybe b
liftMaybe f (Just x) = Just (f x)
liftMaybe _ Nothing = Nothing
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (x : xs) (y : ys) = ((f x) y : ((zipWith f) xs) ys)
zipWith _ [] [] = []
zipWith _ (_ : _) [] = []
zipWith _ [] (_ : _) = []
foo :: ((a -> b) -> a -> b) -> (a -> b) -> a -> b
foo f g a = (f g) a
splunge :: [Nat] -> [Bool] -> [Nat]
splunge ns bs
= ((zipWith (\ n b -> if b then Succ (Succ n) else n)) ns) bs
etad :: [Nat] -> [Bool] -> [Nat]
etad = zipWith (\ n b -> if b then Succ (Succ n) else n)
type LeftSym1 (t0123456789876543210 :: a0123456789876543210) =
Left t0123456789876543210
instance SuppressUnusedWarnings LeftSym0 where
suppressUnusedWarnings = snd (((,) LeftSym0KindInference) ())
data LeftSym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) a0123456789876543210 (Either a0123456789876543210 b0123456789876543210)
where
LeftSym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply LeftSym0 arg) (LeftSym1 arg) =>
LeftSym0 t0123456789876543210
type instance Apply LeftSym0 t0123456789876543210 = Left t0123456789876543210
type RightSym1 (t0123456789876543210 :: b0123456789876543210) =
Right t0123456789876543210
instance SuppressUnusedWarnings RightSym0 where
suppressUnusedWarnings = snd (((,) RightSym0KindInference) ())
data RightSym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) b0123456789876543210 (Either a0123456789876543210 b0123456789876543210)
where
RightSym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply RightSym0 arg) (RightSym1 arg) =>
RightSym0 t0123456789876543210
type instance Apply RightSym0 t0123456789876543210 = Right t0123456789876543210
type family Case_0123456789876543210 ns bs n b t where
Case_0123456789876543210 ns bs n b 'True = Apply SuccSym0 (Apply SuccSym0 n)
Case_0123456789876543210 ns bs n b 'False = n
type family Lambda_0123456789876543210 ns bs t t where
Lambda_0123456789876543210 ns bs n b = Case_0123456789876543210 ns bs n b b
type Lambda_0123456789876543210Sym4 ns0123456789876543210 bs0123456789876543210 t0123456789876543210 t0123456789876543210 =
Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 t0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 t0123456789876543210 bs0123456789876543210 ns0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym3KindInference) ())
data Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 t0123456789876543210 t0123456789876543210
where
Lambda_0123456789876543210Sym3KindInference :: forall ns0123456789876543210
bs0123456789876543210
t0123456789876543210
t0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 t0123456789876543210) arg) (Lambda_0123456789876543210Sym4 ns0123456789876543210 bs0123456789876543210 t0123456789876543210 arg) =>
Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 t0123456789876543210 t0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym3 t0123456789876543210 bs0123456789876543210 ns0123456789876543210) t0123456789876543210 = Lambda_0123456789876543210 t0123456789876543210 bs0123456789876543210 ns0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 bs0123456789876543210 ns0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
data Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 t0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: forall ns0123456789876543210
bs0123456789876543210
t0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210) arg) (Lambda_0123456789876543210Sym3 ns0123456789876543210 bs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 t0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 bs0123456789876543210 ns0123456789876543210) t0123456789876543210 = Lambda_0123456789876543210Sym3 bs0123456789876543210 ns0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 ns0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: forall ns0123456789876543210
bs0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym1 ns0123456789876543210) arg) (Lambda_0123456789876543210Sym2 ns0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 ns0123456789876543210) bs0123456789876543210 = Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym0 ns0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: forall ns0123456789876543210
arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 ns0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 ns0123456789876543210 = Lambda_0123456789876543210Sym1 ns0123456789876543210
type family Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'True = Apply SuccSym0 (Apply SuccSym0 n)
Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'False = n
type family Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 t t where
Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n b = Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 b
type Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210 t0123456789876543210 =
Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 t0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym3KindInference) ())
data Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210 t0123456789876543210
where
Lambda_0123456789876543210Sym3KindInference :: forall a_01234567898765432100123456789876543210
a_01234567898765432100123456789876543210
t0123456789876543210
t0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210) arg) (Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210 arg) =>
Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210 t0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym3 t0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) t0123456789876543210 = Lambda_0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
data Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: forall a_01234567898765432100123456789876543210
a_01234567898765432100123456789876543210
t0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) t0123456789876543210 = Lambda_0123456789876543210Sym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: forall a_01234567898765432100123456789876543210
a_01234567898765432100123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: forall a_01234567898765432100123456789876543210
arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210
type FooSym3 (a0123456789876543210 :: (~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210)) (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (a0123456789876543210 :: a0123456789876543210) =
Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (FooSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) FooSym2KindInference) ())
data FooSym2 (a0123456789876543210 :: (~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210)) (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) :: (~>) a0123456789876543210 b0123456789876543210
where
FooSym2KindInference :: forall a0123456789876543210
a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (FooSym2 a0123456789876543210 a0123456789876543210) arg) (FooSym3 a0123456789876543210 a0123456789876543210 arg) =>
FooSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (FooSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (FooSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) FooSym1KindInference) ())
data FooSym1 (a0123456789876543210 :: (~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210)) :: (~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210)
where
FooSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (FooSym1 a0123456789876543210) arg) (FooSym2 a0123456789876543210 arg) =>
FooSym1 a0123456789876543210 a0123456789876543210
type instance Apply (FooSym1 a0123456789876543210) a0123456789876543210 = FooSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings FooSym0 where
suppressUnusedWarnings = snd (((,) FooSym0KindInference) ())
data FooSym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) ((~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210)) ((~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) a0123456789876543210 b0123456789876543210))
where
FooSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
FooSym0 a0123456789876543210
type instance Apply FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
type ZipWithSym3 (a0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 c0123456789876543210)) (a0123456789876543210 :: [a0123456789876543210]) (a0123456789876543210 :: [b0123456789876543210]) =
ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ZipWithSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) ZipWithSym2KindInference) ())
data ZipWithSym2 (a0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 c0123456789876543210)) (a0123456789876543210 :: [a0123456789876543210]) :: (~>) [b0123456789876543210] [c0123456789876543210]
where
ZipWithSym2KindInference :: forall a0123456789876543210
a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (ZipWithSym2 a0123456789876543210 a0123456789876543210) arg) (ZipWithSym3 a0123456789876543210 a0123456789876543210 arg) =>
ZipWithSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (ZipWithSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ZipWithSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) ZipWithSym1KindInference) ())
data ZipWithSym1 (a0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 c0123456789876543210)) :: (~>) [a0123456789876543210] ((~>) [b0123456789876543210] [c0123456789876543210])
where
ZipWithSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (ZipWithSym1 a0123456789876543210) arg) (ZipWithSym2 a0123456789876543210 arg) =>
ZipWithSym1 a0123456789876543210 a0123456789876543210
type instance Apply (ZipWithSym1 a0123456789876543210) a0123456789876543210 = ZipWithSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ZipWithSym0 where
suppressUnusedWarnings = snd (((,) ZipWithSym0KindInference) ())
data ZipWithSym0 :: forall a0123456789876543210
b0123456789876543210
c0123456789876543210.
(~>) ((~>) a0123456789876543210 ((~>) b0123456789876543210 c0123456789876543210)) ((~>) [a0123456789876543210] ((~>) [b0123456789876543210] [c0123456789876543210]))
where
ZipWithSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply ZipWithSym0 arg) (ZipWithSym1 arg) =>
ZipWithSym0 a0123456789876543210
type instance Apply ZipWithSym0 a0123456789876543210 = ZipWithSym1 a0123456789876543210
type SplungeSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) =
Splunge a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (SplungeSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) SplungeSym1KindInference) ())
data SplungeSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
where
SplungeSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (SplungeSym1 a0123456789876543210) arg) (SplungeSym2 a0123456789876543210 arg) =>
SplungeSym1 a0123456789876543210 a0123456789876543210
type instance Apply (SplungeSym1 a0123456789876543210) a0123456789876543210 = Splunge a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings SplungeSym0 where
suppressUnusedWarnings = snd (((,) SplungeSym0KindInference) ())
data SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
where
SplungeSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply SplungeSym0 arg) (SplungeSym1 arg) =>
SplungeSym0 a0123456789876543210
type instance Apply SplungeSym0 a0123456789876543210 = SplungeSym1 a0123456789876543210
type EtadSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) =
Etad a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (EtadSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) EtadSym1KindInference) ())
data EtadSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
where
EtadSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (EtadSym1 a0123456789876543210) arg) (EtadSym2 a0123456789876543210 arg) =>
EtadSym1 a0123456789876543210 a0123456789876543210
type instance Apply (EtadSym1 a0123456789876543210) a0123456789876543210 = Etad a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings EtadSym0 where
suppressUnusedWarnings = snd (((,) EtadSym0KindInference) ())
data EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
where
EtadSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply EtadSym0 arg) (EtadSym1 arg) =>
EtadSym0 a0123456789876543210
type instance Apply EtadSym0 a0123456789876543210 = EtadSym1 a0123456789876543210
type LiftMaybeSym2 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (a0123456789876543210 :: Maybe a0123456789876543210) =
LiftMaybe a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) LiftMaybeSym1KindInference) ())
data LiftMaybeSym1 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) :: (~>) (Maybe a0123456789876543210) (Maybe b0123456789876543210)
where
LiftMaybeSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (LiftMaybeSym1 a0123456789876543210) arg) (LiftMaybeSym2 a0123456789876543210 arg) =>
LiftMaybeSym1 a0123456789876543210 a0123456789876543210
type instance Apply (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings LiftMaybeSym0 where
suppressUnusedWarnings = snd (((,) LiftMaybeSym0KindInference) ())
data LiftMaybeSym0 :: forall a0123456789876543210
b0123456789876543210.
(~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) (Maybe a0123456789876543210) (Maybe b0123456789876543210))
where
LiftMaybeSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
LiftMaybeSym0 a0123456789876543210
type instance Apply LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
type MapSym2 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (a0123456789876543210 :: [a0123456789876543210]) =
Map a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MapSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) MapSym1KindInference) ())
data MapSym1 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) :: (~>) [a0123456789876543210] [b0123456789876543210]
where
MapSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (MapSym1 a0123456789876543210) arg) (MapSym2 a0123456789876543210 arg) =>
MapSym1 a0123456789876543210 a0123456789876543210
type instance Apply (MapSym1 a0123456789876543210) a0123456789876543210 = Map a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings MapSym0 where
suppressUnusedWarnings = snd (((,) MapSym0KindInference) ())
data MapSym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) [a0123456789876543210] [b0123456789876543210])
where
MapSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply MapSym0 arg) (MapSym1 arg) =>
MapSym0 a0123456789876543210
type instance Apply MapSym0 a0123456789876543210 = MapSym1 a0123456789876543210
type family Foo (a :: (~>) ((~>) a b) ((~>) a b)) (a :: (~>) a b) (a :: a) :: b where
Foo f g a = Apply (Apply f g) a
type family ZipWith (a :: (~>) a ((~>) b c)) (a :: [a]) (a :: [b]) :: [c] where
ZipWith f ( '(:) x xs) ( '(:) y ys) = Apply (Apply (:@#@$) (Apply (Apply f x) y)) (Apply (Apply (Apply ZipWithSym0 f) xs) ys)
ZipWith _ '[] '[] = '[]
ZipWith _ ( '(:) _ _) '[] = '[]
ZipWith _ '[] ( '(:) _ _) = '[]
type family Splunge (a :: [Nat]) (a :: [Bool]) :: [Nat] where
Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789876543210Sym0 ns) bs)) ns) bs
type family Etad (a :: [Nat]) (a :: [Bool]) :: [Nat] where
Etad a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210)) a_0123456789876543210) a_0123456789876543210
type family LiftMaybe (a :: (~>) a b) (a :: Maybe a) :: Maybe b where
LiftMaybe f ( 'Just x) = Apply JustSym0 (Apply f x)
LiftMaybe _ 'Nothing = NothingSym0
type family Map (a :: (~>) a b) (a :: [a]) :: [b] where
Map _ '[] = '[]
Map f ( '(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t)
sFoo ::
forall a
b
(t :: (~>) ((~>) a b) ((~>) a b))
(t :: (~>) a b)
(t :: a).
Sing t
-> Sing t
-> Sing t -> Sing (Apply (Apply (Apply FooSym0 t) t) t :: b)
sZipWith ::
forall a b c (t :: (~>) a ((~>) b c)) (t :: [a]) (t :: [b]).
Sing t
-> Sing t
-> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c])
sSplunge ::
forall (t :: [Nat]) (t :: [Bool]).
Sing t -> Sing t -> Sing (Apply (Apply SplungeSym0 t) t :: [Nat])
sEtad ::
forall (t :: [Nat]) (t :: [Bool]).
Sing t -> Sing t -> Sing (Apply (Apply EtadSym0 t) t :: [Nat])
sLiftMaybe ::
forall a b (t :: (~>) a b) (t :: Maybe a).
Sing t
-> Sing t -> Sing (Apply (Apply LiftMaybeSym0 t) t :: Maybe b)
sMap ::
forall a b (t :: (~>) a b) (t :: [a]).
Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b])
sFoo (sF :: Sing f) (sG :: Sing g) (sA :: Sing a)
= (applySing ((applySing sF) sG)) sA
sZipWith
(sF :: Sing f)
(SCons (sX :: Sing x) (sXs :: Sing xs))
(SCons (sY :: Sing y) (sYs :: Sing ys))
= (applySing
((applySing ((singFun2 @(:@#@$)) SCons))
((applySing ((applySing sF) sX)) sY)))
((applySing
((applySing ((applySing ((singFun3 @ZipWithSym0) sZipWith)) sF))
sXs))
sYs)
sZipWith _ SNil SNil = SNil
sZipWith _ (SCons _ _) SNil = SNil
sZipWith _ SNil (SCons _ _) = SNil
sSplunge (sNs :: Sing ns) (sBs :: Sing bs)
= (applySing
((applySing
((applySing ((singFun3 @ZipWithSym0) sZipWith))
((singFun2 @(Apply (Apply Lambda_0123456789876543210Sym0 ns) bs))
(\ sN sB
-> case ((,) sN) sB of {
(,) (_ :: Sing n) (_ :: Sing b)
-> (case sB of
STrue
-> (applySing ((singFun1 @SuccSym0) SSucc))
((applySing ((singFun1 @SuccSym0) SSucc)) sN)
SFalse -> sN) ::
Sing (Case_0123456789876543210 ns bs n b b) }))))
sNs))
sBs
sEtad
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing
((applySing ((singFun3 @ZipWithSym0) sZipWith))
((singFun2
@(Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210))
(\ sN sB
-> case ((,) sN) sB of {
(,) (_ :: Sing n) (_ :: Sing b)
-> (case sB of
STrue
-> (applySing ((singFun1 @SuccSym0) SSucc))
((applySing ((singFun1 @SuccSym0) SSucc)) sN)
SFalse -> sN) ::
Sing (Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 b) }))))
sA_0123456789876543210))
sA_0123456789876543210
sLiftMaybe (sF :: Sing f) (SJust (sX :: Sing x))
= (applySing ((singFun1 @JustSym0) SJust)) ((applySing sF) sX)
sLiftMaybe _ SNothing = SNothing
sMap _ SNil = SNil
sMap (sF :: Sing f) (SCons (sH :: Sing h) (sT :: Sing t))
= (applySing
((applySing ((singFun2 @(:@#@$)) SCons)) ((applySing sF) sH)))
((applySing ((applySing ((singFun2 @MapSym0) sMap)) sF)) sT)
instance SingI (FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))) where
sing = (singFun3 @FooSym0) sFoo
instance SingI d =>
SingI (FooSym1 (d :: (~>) ((~>) a b) ((~>) a b)) :: (~>) ((~>) a b) ((~>) a b)) where
sing
= (singFun2 @(FooSym1 (d :: (~>) ((~>) a b) ((~>) a b))))
(sFoo (sing @d))
instance (SingI d, SingI d) =>
SingI (FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b) :: (~>) a b) where
sing
= (singFun1
@(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b)))
((sFoo (sing @d)) (sing @d))
instance SingI (ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))) where
sing = (singFun3 @ZipWithSym0) sZipWith
instance SingI d =>
SingI (ZipWithSym1 (d :: (~>) a ((~>) b c)) :: (~>) [a] ((~>) [b] [c])) where
sing
= (singFun2 @(ZipWithSym1 (d :: (~>) a ((~>) b c))))
(sZipWith (sing @d))
instance (SingI d, SingI d) =>
SingI (ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a]) :: (~>) [b] [c]) where
sing
= (singFun1 @(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a])))
((sZipWith (sing @d)) (sing @d))
instance SingI (SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])) where
sing = (singFun2 @SplungeSym0) sSplunge
instance SingI d =>
SingI (SplungeSym1 (d :: [Nat]) :: (~>) [Bool] [Nat]) where
sing = (singFun1 @(SplungeSym1 (d :: [Nat]))) (sSplunge (sing @d))
instance SingI (EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])) where
sing = (singFun2 @EtadSym0) sEtad
instance SingI d =>
SingI (EtadSym1 (d :: [Nat]) :: (~>) [Bool] [Nat]) where
sing = (singFun1 @(EtadSym1 (d :: [Nat]))) (sEtad (sing @d))
instance SingI (LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))) where
sing = (singFun2 @LiftMaybeSym0) sLiftMaybe
instance SingI d =>
SingI (LiftMaybeSym1 (d :: (~>) a b) :: (~>) (Maybe a) (Maybe b)) where
sing
= (singFun1 @(LiftMaybeSym1 (d :: (~>) a b)))
(sLiftMaybe (sing @d))
instance SingI (MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])) where
sing = (singFun2 @MapSym0) sMap
instance SingI d =>
SingI (MapSym1 (d :: (~>) a b) :: (~>) [a] [b]) where
sing = (singFun1 @(MapSym1 (d :: (~>) a b))) (sMap (sing @d))
data instance Sing :: Either a b -> GHC.Types.Type
where
SLeft :: forall a (n :: a). (Sing (n :: a)) -> Sing (Left n)
SRight :: forall b (n :: b). (Sing (n :: b)) -> Sing (Right n)
type SEither = (Sing :: Either a b -> GHC.Types.Type)
instance (SingKind a, SingKind b) => SingKind (Either a b) where
type Demote (Either a b) = Either (Demote a) (Demote b)
fromSing (SLeft b) = Left (fromSing b)
fromSing (SRight b) = Right (fromSing b)
toSing (Left (b :: Demote a))
= case toSing b :: SomeSing a of {
SomeSing c -> SomeSing (SLeft c) }
toSing (Right (b :: Demote b))
= case toSing b :: SomeSing b of {
SomeSing c -> SomeSing (SRight c) }
instance SingI n => SingI (Left (n :: a)) where
sing = SLeft sing
instance SingI (LeftSym0 :: (~>) a (Either a b)) where
sing = (singFun1 @LeftSym0) SLeft
instance SingI (TyCon1 Left :: (~>) a (Either a b)) where
sing = (singFun1 @(TyCon1 Left)) SLeft
instance SingI n => SingI (Right (n :: b)) where
sing = SRight sing
instance SingI (RightSym0 :: (~>) b (Either a b)) where
sing = (singFun1 @RightSym0) SRight
instance SingI (TyCon1 Right :: (~>) b (Either a b)) where
sing = (singFun1 @(TyCon1 Right)) SRight