singletons-base-3.5: tests/compile-and-dump/Singletons/HigherOrder.golden
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 LeftSym0 :: forall a b. (~>) a (Either a b)
data LeftSym0 :: (~>) a (Either a b)
where
LeftSym0KindInference :: SameKind (Apply LeftSym0 arg) (LeftSym1 arg) =>
LeftSym0 a0123456789876543210
type instance Apply @a @(Either a b) LeftSym0 a0123456789876543210 = Left a0123456789876543210
instance SuppressUnusedWarnings LeftSym0 where
suppressUnusedWarnings = snd ((,) LeftSym0KindInference ())
type LeftSym1 :: forall a b. a -> Either a b
type family LeftSym1 @a @b (a0123456789876543210 :: a) :: Either a b where
LeftSym1 a0123456789876543210 = Left a0123456789876543210
type RightSym0 :: forall a b. (~>) b (Either a b)
data RightSym0 :: (~>) b (Either a b)
where
RightSym0KindInference :: SameKind (Apply RightSym0 arg) (RightSym1 arg) =>
RightSym0 a0123456789876543210
type instance Apply @b @(Either a b) RightSym0 a0123456789876543210 = Right a0123456789876543210
instance SuppressUnusedWarnings RightSym0 where
suppressUnusedWarnings = snd ((,) RightSym0KindInference ())
type RightSym1 :: forall a b. b -> Either a b
type family RightSym1 @a @b (a0123456789876543210 :: b) :: Either a b where
RightSym1 a0123456789876543210 = Right a0123456789876543210
type family LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_0123456789876543210 where
LamCases_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'True = Apply SuccSym0 (Apply SuccSym0 n)
LamCases_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'False = n
data LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n b = Apply (LamCases_0123456789876543210Sym0 n b a_0123456789876543210 a_0123456789876543210) b
data LamCases_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
data LamCases_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym1KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym1KindInference ())
type family LamCases_0123456789876543210Sym2 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_0123456789876543210 where
LamCases_0123456789876543210 n b ns bs 'True = Apply SuccSym0 (Apply SuccSym0 n)
LamCases_0123456789876543210 n b ns bs 'False = n
data LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210) arg) (LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ns bs n b = Apply (LamCases_0123456789876543210Sym0 n b ns bs) b
data LamCases_0123456789876543210Sym0 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210) arg) (LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
data LamCases_0123456789876543210Sym1 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym1KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym1KindInference ())
type family LamCases_0123456789876543210Sym2 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 ns0123456789876543210 bs0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
data EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
where
EtadSym0KindInference :: SameKind (Apply EtadSym0 arg) (EtadSym1 arg) =>
EtadSym0 a0123456789876543210
type instance Apply @[Nat] @((~>) [Bool] [Nat]) EtadSym0 a0123456789876543210 = EtadSym1 a0123456789876543210
instance SuppressUnusedWarnings EtadSym0 where
suppressUnusedWarnings = snd ((,) EtadSym0KindInference ())
type EtadSym1 :: [Nat] -> (~>) [Bool] [Nat]
data EtadSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
where
EtadSym1KindInference :: SameKind (Apply (EtadSym1 a0123456789876543210) arg) (EtadSym2 a0123456789876543210 arg) =>
EtadSym1 a0123456789876543210 a0123456789876543210
type instance Apply @[Bool] @[Nat] (EtadSym1 a0123456789876543210) a0123456789876543210 = Etad a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (EtadSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) EtadSym1KindInference ())
type EtadSym2 :: [Nat] -> [Bool] -> [Nat]
type family EtadSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) :: [Nat] where
EtadSym2 a0123456789876543210 a0123456789876543210 = Etad a0123456789876543210 a0123456789876543210
type SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
data SplungeSym0 :: (~>) [Nat] ((~>) [Bool] [Nat])
where
SplungeSym0KindInference :: SameKind (Apply SplungeSym0 arg) (SplungeSym1 arg) =>
SplungeSym0 a0123456789876543210
type instance Apply @[Nat] @((~>) [Bool] [Nat]) SplungeSym0 a0123456789876543210 = SplungeSym1 a0123456789876543210
instance SuppressUnusedWarnings SplungeSym0 where
suppressUnusedWarnings = snd ((,) SplungeSym0KindInference ())
type SplungeSym1 :: [Nat] -> (~>) [Bool] [Nat]
data SplungeSym1 (a0123456789876543210 :: [Nat]) :: (~>) [Bool] [Nat]
where
SplungeSym1KindInference :: SameKind (Apply (SplungeSym1 a0123456789876543210) arg) (SplungeSym2 a0123456789876543210 arg) =>
SplungeSym1 a0123456789876543210 a0123456789876543210
type instance Apply @[Bool] @[Nat] (SplungeSym1 a0123456789876543210) a0123456789876543210 = Splunge a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (SplungeSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) SplungeSym1KindInference ())
type SplungeSym2 :: [Nat] -> [Bool] -> [Nat]
type family SplungeSym2 (a0123456789876543210 :: [Nat]) (a0123456789876543210 :: [Bool]) :: [Nat] where
SplungeSym2 a0123456789876543210 a0123456789876543210 = Splunge a0123456789876543210 a0123456789876543210
type FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))
data FooSym0 :: (~>) ((~>) ((~>) a b) ((~>) a b)) ((~>) ((~>) a b) ((~>) a b))
where
FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
FooSym0 a0123456789876543210
type instance Apply @((~>) ((~>) a b) ((~>) a b)) @((~>) ((~>) a b) ((~>) a b)) FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
instance SuppressUnusedWarnings FooSym0 where
suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
type FooSym1 :: (~>) ((~>) a b) ((~>) a b)
-> (~>) ((~>) a b) ((~>) a b)
data FooSym1 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) :: (~>) ((~>) a b) ((~>) a b)
where
FooSym1KindInference :: SameKind (Apply (FooSym1 a0123456789876543210) arg) (FooSym2 a0123456789876543210 arg) =>
FooSym1 a0123456789876543210 a0123456789876543210
type instance Apply @((~>) a b) @((~>) a b) (FooSym1 a0123456789876543210) a0123456789876543210 = FooSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (FooSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) FooSym1KindInference ())
type FooSym2 :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> (~>) a b
data FooSym2 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) :: (~>) a b
where
FooSym2KindInference :: SameKind (Apply (FooSym2 a0123456789876543210 a0123456789876543210) arg) (FooSym3 a0123456789876543210 a0123456789876543210 arg) =>
FooSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply @a @b (FooSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (FooSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) FooSym2KindInference ())
type FooSym3 :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b
type family FooSym3 @a @b (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: a) :: b where
FooSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210
type ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))
data ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c]))
where
ZipWithSym0KindInference :: SameKind (Apply ZipWithSym0 arg) (ZipWithSym1 arg) =>
ZipWithSym0 a0123456789876543210
type instance Apply @((~>) a ((~>) b c)) @((~>) [a] ((~>) [b] [c])) ZipWithSym0 a0123456789876543210 = ZipWithSym1 a0123456789876543210
instance SuppressUnusedWarnings ZipWithSym0 where
suppressUnusedWarnings = snd ((,) ZipWithSym0KindInference ())
type ZipWithSym1 :: (~>) a ((~>) b c) -> (~>) [a] ((~>) [b] [c])
data ZipWithSym1 (a0123456789876543210 :: (~>) a ((~>) b c)) :: (~>) [a] ((~>) [b] [c])
where
ZipWithSym1KindInference :: SameKind (Apply (ZipWithSym1 a0123456789876543210) arg) (ZipWithSym2 a0123456789876543210 arg) =>
ZipWithSym1 a0123456789876543210 a0123456789876543210
type instance Apply @[a] @((~>) [b] [c]) (ZipWithSym1 a0123456789876543210) a0123456789876543210 = ZipWithSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ZipWithSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) ZipWithSym1KindInference ())
type ZipWithSym2 :: (~>) a ((~>) b c) -> [a] -> (~>) [b] [c]
data ZipWithSym2 (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) :: (~>) [b] [c]
where
ZipWithSym2KindInference :: SameKind (Apply (ZipWithSym2 a0123456789876543210 a0123456789876543210) arg) (ZipWithSym3 a0123456789876543210 a0123456789876543210 arg) =>
ZipWithSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply @[b] @[c] (ZipWithSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ZipWithSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) ZipWithSym2KindInference ())
type ZipWithSym3 :: (~>) a ((~>) b c) -> [a] -> [b] -> [c]
type family ZipWithSym3 @a @b @c (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [c] where
ZipWithSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210
type LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
data LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b))
where
LiftMaybeSym0KindInference :: SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
LiftMaybeSym0 a0123456789876543210
type instance Apply @((~>) a b) @((~>) (Maybe a) (Maybe b)) LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
instance SuppressUnusedWarnings LiftMaybeSym0 where
suppressUnusedWarnings = snd ((,) LiftMaybeSym0KindInference ())
type LiftMaybeSym1 :: (~>) a b -> (~>) (Maybe a) (Maybe b)
data LiftMaybeSym1 (a0123456789876543210 :: (~>) a b) :: (~>) (Maybe a) (Maybe b)
where
LiftMaybeSym1KindInference :: SameKind (Apply (LiftMaybeSym1 a0123456789876543210) arg) (LiftMaybeSym2 a0123456789876543210 arg) =>
LiftMaybeSym1 a0123456789876543210 a0123456789876543210
type instance Apply @(Maybe a) @(Maybe b) (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) LiftMaybeSym1KindInference ())
type LiftMaybeSym2 :: (~>) a b -> Maybe a -> Maybe b
type family LiftMaybeSym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where
LiftMaybeSym2 a0123456789876543210 a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
type MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])
data MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b])
where
MapSym0KindInference :: SameKind (Apply MapSym0 arg) (MapSym1 arg) =>
MapSym0 a0123456789876543210
type instance Apply @((~>) a b) @((~>) [a] [b]) MapSym0 a0123456789876543210 = MapSym1 a0123456789876543210
instance SuppressUnusedWarnings MapSym0 where
suppressUnusedWarnings = snd ((,) MapSym0KindInference ())
type MapSym1 :: (~>) a b -> (~>) [a] [b]
data MapSym1 (a0123456789876543210 :: (~>) a b) :: (~>) [a] [b]
where
MapSym1KindInference :: SameKind (Apply (MapSym1 a0123456789876543210) arg) (MapSym2 a0123456789876543210 arg) =>
MapSym1 a0123456789876543210 a0123456789876543210
type instance Apply @[a] @[b] (MapSym1 a0123456789876543210) a0123456789876543210 = Map a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MapSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MapSym1KindInference ())
type MapSym2 :: (~>) a b -> [a] -> [b]
type family MapSym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: [a]) :: [b] where
MapSym2 a0123456789876543210 a0123456789876543210 = Map a0123456789876543210 a0123456789876543210
type Etad :: [Nat] -> [Bool] -> [Nat]
type family Etad (a :: [Nat]) (a :: [Bool]) :: [Nat] where
Etad a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Apply ZipWithSym0 (LamCases_0123456789876543210Sym0 a_0123456789876543210 a_0123456789876543210)) a_0123456789876543210) a_0123456789876543210
type Splunge :: [Nat] -> [Bool] -> [Nat]
type family Splunge (a :: [Nat]) (a :: [Bool]) :: [Nat] where
Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (LamCases_0123456789876543210Sym0 ns bs)) ns) bs
type Foo :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b
type family Foo @a @b (a :: (~>) ((~>) a b) ((~>) a b)) (a :: (~>) a b) (a :: a) :: b where
Foo f g a = Apply (Apply f g) a
type ZipWith :: (~>) a ((~>) b c) -> [a] -> [b] -> [c]
type family ZipWith @a @b @c (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 _ '[] '[] = NilSym0
ZipWith _ ('(:) _ _) '[] = NilSym0
ZipWith _ '[] ('(:) _ _) = NilSym0
type LiftMaybe :: (~>) a b -> Maybe a -> Maybe b
type family LiftMaybe @a @b (a :: (~>) a b) (a :: Maybe a) :: Maybe b where
LiftMaybe f ('Just x) = Apply JustSym0 (Apply f x)
LiftMaybe _ 'Nothing = NothingSym0
type Map :: (~>) a b -> [a] -> [b]
type family Map @a @b (a :: (~>) a b) (a :: [a]) :: [b] where
Map _ '[] = NilSym0
Map f ('(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t)
sEtad ::
(forall (t :: [Nat]) (t :: [Bool]).
Sing t -> Sing t -> Sing (Etad t t :: [Nat]) :: Type)
sSplunge ::
(forall (t :: [Nat]) (t :: [Bool]).
Sing t -> Sing t -> Sing (Splunge t t :: [Nat]) :: Type)
sFoo ::
(forall (t :: (~>) ((~>) a b) ((~>) a b)) (t :: (~>) a b) (t :: a).
Sing t -> Sing t -> Sing t -> Sing (Foo t t t :: b) :: Type)
sZipWith ::
(forall (t :: (~>) a ((~>) b c)) (t :: [a]) (t :: [b]).
Sing t -> Sing t -> Sing t -> Sing (ZipWith t t t :: [c]) :: Type)
sLiftMaybe ::
(forall (t :: (~>) a b) (t :: Maybe a).
Sing t -> Sing t -> Sing (LiftMaybe t t :: Maybe b) :: Type)
sMap ::
(forall (t :: (~>) a b) (t :: [a]).
Sing t -> Sing t -> Sing (Map t t :: [b]) :: Type)
sEtad
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ZipWithSym0 sZipWith)
(singFun2
@(LamCases_0123456789876543210Sym0 a_0123456789876543210 a_0123456789876543210)
(\cases
(sN :: Sing n) (sB :: Sing b)
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 n b a_0123456789876543210 a_0123456789876543210)
(\cases
STrue
-> applySing
(singFun1 @SuccSym0 SSucc)
(applySing (singFun1 @SuccSym0 SSucc) sN)
SFalse -> sN))
sB)))
sA_0123456789876543210)
sA_0123456789876543210
sSplunge (sNs :: Sing ns) (sBs :: Sing bs)
= applySing
(applySing
(applySing
(singFun3 @ZipWithSym0 sZipWith)
(singFun2
@(LamCases_0123456789876543210Sym0 ns bs)
(\cases
(sN :: Sing n) (sB :: Sing b)
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 n b ns bs)
(\cases
STrue
-> applySing
(singFun1 @SuccSym0 SSucc)
(applySing (singFun1 @SuccSym0 SSucc) sN)
SFalse -> sN))
sB)))
sNs)
sBs
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
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 (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 SingI1 (EtadSym1 :: [Nat] -> (~>) [Bool] [Nat]) where
liftSing (s :: Sing (d :: [Nat]))
= singFun1 @(EtadSym1 (d :: [Nat])) (sEtad s)
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 SingI1 (SplungeSym1 :: [Nat] -> (~>) [Bool] [Nat]) where
liftSing (s :: Sing (d :: [Nat]))
= singFun1 @(SplungeSym1 (d :: [Nat])) (sSplunge s)
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 SingI1 (FooSym1 :: (~>) ((~>) a b) ((~>) a b)
-> (~>) ((~>) a b) ((~>) a b)) where
liftSing (s :: Sing (d :: (~>) ((~>) a b) ((~>) a b)))
= singFun2 @(FooSym1 (d :: (~>) ((~>) a b) ((~>) a b))) (sFoo s)
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 d =>
SingI1 (FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) :: (~>) a b
-> (~>) a b) where
liftSing (s :: Sing (d :: (~>) a b))
= singFun1
@(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b))
(sFoo (sing @d) s)
instance SingI2 (FooSym2 :: (~>) ((~>) a b) ((~>) a b)
-> (~>) a b -> (~>) a b) where
liftSing2
(s :: Sing (d :: (~>) ((~>) a b) ((~>) a b)))
(s :: Sing (d :: (~>) a b))
= singFun1
@(FooSym2 (d :: (~>) ((~>) a b) ((~>) a b)) (d :: (~>) a b))
(sFoo s s)
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 SingI1 (ZipWithSym1 :: (~>) a ((~>) b c)
-> (~>) [a] ((~>) [b] [c])) where
liftSing (s :: Sing (d :: (~>) a ((~>) b c)))
= singFun2 @(ZipWithSym1 (d :: (~>) a ((~>) b c))) (sZipWith s)
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 d =>
SingI1 (ZipWithSym2 (d :: (~>) a ((~>) b c)) :: [a]
-> (~>) [b] [c]) where
liftSing (s :: Sing (d :: [a]))
= singFun1
@(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a]))
(sZipWith (sing @d) s)
instance SingI2 (ZipWithSym2 :: (~>) a ((~>) b c)
-> [a] -> (~>) [b] [c]) where
liftSing2
(s :: Sing (d :: (~>) a ((~>) b c)))
(s :: Sing (d :: [a]))
= singFun1
@(ZipWithSym2 (d :: (~>) a ((~>) b c)) (d :: [a])) (sZipWith s s)
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 SingI1 (LiftMaybeSym1 :: (~>) a b
-> (~>) (Maybe a) (Maybe b)) where
liftSing (s :: Sing (d :: (~>) a b))
= singFun1 @(LiftMaybeSym1 (d :: (~>) a b)) (sLiftMaybe s)
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))
instance SingI1 (MapSym1 :: (~>) a b -> (~>) [a] [b]) where
liftSing (s :: Sing (d :: (~>) a b))
= singFun1 @(MapSym1 (d :: (~>) a b)) (sMap s)
data SEither :: forall a b. Either a b -> Type
where
SLeft :: forall a b (n :: a).
(Sing n) -> SEither (Left n :: Either a b)
SRight :: forall a b (n :: b).
(Sing n) -> SEither (Right n :: Either a b)
type instance Sing @(Either a b) = SEither
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))
= (\cases (SomeSing c) -> SomeSing (SLeft c))
(toSing b :: SomeSing a)
toSing (Right (b :: Demote b))
= (\cases (SomeSing c) -> SomeSing (SRight c))
(toSing b :: SomeSing b)
instance SingI n => SingI (Left (n :: a)) where
sing = SLeft sing
instance SingI1 Left where
liftSing = SLeft
instance SingI (LeftSym0 :: (~>) a (Either a b)) where
sing = singFun1 @LeftSym0 SLeft
instance SingI n => SingI (Right (n :: b)) where
sing = SRight sing
instance SingI1 Right where
liftSing = SRight
instance SingI (RightSym0 :: (~>) b (Either a b)) where
sing = singFun1 @RightSym0 SRight