singletons-1.0: tests/compile-and-dump/Singletons/HigherOrder.ghc78.template
Singletons/HigherOrder.hs: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 |]
======>
Singletons/HigherOrder.hs:(0,0)-(0,0)
data Either a b = Left a | Right b
map :: forall a b. (a -> b) -> [a] -> [b]
map _ GHC.Types.[] = []
map f (h GHC.Types.: t) = ((f h) GHC.Types.: (map f t))
liftMaybe :: forall a b. (a -> b) -> Maybe a -> Maybe b
liftMaybe f (Just x) = Just (f x)
liftMaybe _ Nothing = Nothing
zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (x GHC.Types.: xs) (y GHC.Types.: ys)
= ((f x y) GHC.Types.: (zipWith f xs ys))
zipWith _ GHC.Types.[] GHC.Types.[] = []
zipWith _ (_ GHC.Types.: _) GHC.Types.[] = []
zipWith _ GHC.Types.[] (_ GHC.Types.: _) = []
foo :: forall a b. ((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 (t :: a) = Left t
instance SuppressUnusedWarnings LeftSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) LeftSym0KindInference GHC.Tuple.())
data LeftSym0 (l :: TyFun a (Either a b))
= forall arg. (GHC.Types.~) (KindOf (Apply LeftSym0 arg)) (KindOf (LeftSym1 arg)) =>
LeftSym0KindInference
type instance Apply LeftSym0 l = LeftSym1 l
type RightSym1 (t :: b) = Right t
instance SuppressUnusedWarnings RightSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) RightSym0KindInference GHC.Tuple.())
data RightSym0 (l :: TyFun b (Either a b))
= forall arg. (GHC.Types.~) (KindOf (Apply RightSym0 arg)) (KindOf (RightSym1 arg)) =>
RightSym0KindInference
type instance Apply RightSym0 l = RightSym1 l
type Let_0123456789Scrutinee_0123456789Sym4 t t t t =
Let_0123456789Scrutinee_0123456789 t t t t
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym3 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym3KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym3 l l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym4 l l l arg)) =>
Let_0123456789Scrutinee_0123456789Sym3KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) l = Let_0123456789Scrutinee_0123456789Sym4 l l l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym2 l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym3 l l arg)) =>
Let_0123456789Scrutinee_0123456789Sym2KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) l = Let_0123456789Scrutinee_0123456789Sym3 l l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym1 l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym1 l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym2 l arg)) =>
Let_0123456789Scrutinee_0123456789Sym1KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym1 l) l = Let_0123456789Scrutinee_0123456789Sym2 l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym0 l
= forall arg. (GHC.Types.~) (KindOf (Apply Let_0123456789Scrutinee_0123456789Sym0 arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym1 arg)) =>
Let_0123456789Scrutinee_0123456789Sym0KindInference
type instance Apply Let_0123456789Scrutinee_0123456789Sym0 l = Let_0123456789Scrutinee_0123456789Sym1 l
type Let_0123456789Scrutinee_0123456789 ns bs n b = b
type family Case_0123456789 ns bs n b t where
Case_0123456789 ns bs n b True = Apply SuccSym0 (Apply SuccSym0 n)
Case_0123456789 ns bs n b False = n
type family Lambda_0123456789 ns bs t t where
Lambda_0123456789 ns bs n b = Case_0123456789 ns bs n b (Let_0123456789Scrutinee_0123456789Sym4 ns bs n b)
type Lambda_0123456789Sym4 t t t t = Lambda_0123456789 t t t t
instance SuppressUnusedWarnings Lambda_0123456789Sym3 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym3KindInference GHC.Tuple.())
data Lambda_0123456789Sym3 l l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym3 l l l) arg)) (KindOf (Lambda_0123456789Sym4 l l l arg)) =>
Lambda_0123456789Sym3KindInference
type instance Apply (Lambda_0123456789Sym3 l l l) l = Lambda_0123456789Sym4 l l l l
instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
data Lambda_0123456789Sym2 l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym2 l l) arg)) (KindOf (Lambda_0123456789Sym3 l l arg)) =>
Lambda_0123456789Sym2KindInference
type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
data Lambda_0123456789Sym1 l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym1 l) arg)) (KindOf (Lambda_0123456789Sym2 l arg)) =>
Lambda_0123456789Sym1KindInference
type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
data Lambda_0123456789Sym0 l
= forall arg. (GHC.Types.~) (KindOf (Apply Lambda_0123456789Sym0 arg)) (KindOf (Lambda_0123456789Sym1 arg)) =>
Lambda_0123456789Sym0KindInference
type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
type Let_0123456789Scrutinee_0123456789Sym4 t t t t =
Let_0123456789Scrutinee_0123456789 t t t t
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym3 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym3KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym3 l l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym4 l l l arg)) =>
Let_0123456789Scrutinee_0123456789Sym3KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) l = Let_0123456789Scrutinee_0123456789Sym4 l l l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym2 l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym3 l l arg)) =>
Let_0123456789Scrutinee_0123456789Sym2KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) l = Let_0123456789Scrutinee_0123456789Sym3 l l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym1 l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym1 l) arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym2 l arg)) =>
Let_0123456789Scrutinee_0123456789Sym1KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym1 l) l = Let_0123456789Scrutinee_0123456789Sym2 l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym0 l
= forall arg. (GHC.Types.~) (KindOf (Apply Let_0123456789Scrutinee_0123456789Sym0 arg)) (KindOf (Let_0123456789Scrutinee_0123456789Sym1 arg)) =>
Let_0123456789Scrutinee_0123456789Sym0KindInference
type instance Apply Let_0123456789Scrutinee_0123456789Sym0 l = Let_0123456789Scrutinee_0123456789Sym1 l
type Let_0123456789Scrutinee_0123456789 n
b
a_0123456789
a_0123456789 =
b
type family Case_0123456789 n b a_0123456789 a_0123456789 t where
Case_0123456789 n b a_0123456789 a_0123456789 True = Apply SuccSym0 (Apply SuccSym0 n)
Case_0123456789 n b a_0123456789 a_0123456789 False = n
type family Lambda_0123456789 a_0123456789 a_0123456789 t t where
Lambda_0123456789 a_0123456789 a_0123456789 n b = Case_0123456789 n b a_0123456789 a_0123456789 (Let_0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789)
type Lambda_0123456789Sym4 t t t t = Lambda_0123456789 t t t t
instance SuppressUnusedWarnings Lambda_0123456789Sym3 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym3KindInference GHC.Tuple.())
data Lambda_0123456789Sym3 l l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym3 l l l) arg)) (KindOf (Lambda_0123456789Sym4 l l l arg)) =>
Lambda_0123456789Sym3KindInference
type instance Apply (Lambda_0123456789Sym3 l l l) l = Lambda_0123456789Sym4 l l l l
instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
data Lambda_0123456789Sym2 l l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym2 l l) arg)) (KindOf (Lambda_0123456789Sym3 l l arg)) =>
Lambda_0123456789Sym2KindInference
type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
data Lambda_0123456789Sym1 l l
= forall arg. (GHC.Types.~) (KindOf (Apply (Lambda_0123456789Sym1 l) arg)) (KindOf (Lambda_0123456789Sym2 l arg)) =>
Lambda_0123456789Sym1KindInference
type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
data Lambda_0123456789Sym0 l
= forall arg. (GHC.Types.~) (KindOf (Apply Lambda_0123456789Sym0 arg)) (KindOf (Lambda_0123456789Sym1 arg)) =>
Lambda_0123456789Sym0KindInference
type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
type FooSym3 (t :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
(t :: TyFun a b -> *)
(t :: a) =
Foo t t t
instance SuppressUnusedWarnings FooSym2 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) FooSym2KindInference GHC.Tuple.())
data FooSym2 (l :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
(l :: TyFun a b -> *)
(l :: TyFun a b)
= forall arg. (GHC.Types.~) (KindOf (Apply (FooSym2 l l) arg)) (KindOf (FooSym3 l l arg)) =>
FooSym2KindInference
type instance Apply (FooSym2 l l) l = FooSym3 l l l
instance SuppressUnusedWarnings FooSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) FooSym1KindInference GHC.Tuple.())
data FooSym1 (l :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
(l :: TyFun (TyFun a b -> *) (TyFun a b -> *))
= forall arg. (GHC.Types.~) (KindOf (Apply (FooSym1 l) arg)) (KindOf (FooSym2 l arg)) =>
FooSym1KindInference
type instance Apply (FooSym1 l) l = FooSym2 l l
instance SuppressUnusedWarnings FooSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) FooSym0KindInference GHC.Tuple.())
data FooSym0 (l :: TyFun (TyFun (TyFun a b -> *) (TyFun a b -> *)
-> *) (TyFun (TyFun a b -> *) (TyFun a b -> *) -> *))
= forall arg. (GHC.Types.~) (KindOf (Apply FooSym0 arg)) (KindOf (FooSym1 arg)) =>
FooSym0KindInference
type instance Apply FooSym0 l = FooSym1 l
type ZipWithSym3 (t :: TyFun a (TyFun b c -> *) -> *)
(t :: GHC.Types.[] a)
(t :: GHC.Types.[] b) =
ZipWith t t t
instance SuppressUnusedWarnings ZipWithSym2 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) ZipWithSym2KindInference GHC.Tuple.())
data ZipWithSym2 (l :: TyFun a (TyFun b c -> *) -> *)
(l :: GHC.Types.[] a)
(l :: TyFun (GHC.Types.[] b) (GHC.Types.[] c))
= forall arg. (GHC.Types.~) (KindOf (Apply (ZipWithSym2 l l) arg)) (KindOf (ZipWithSym3 l l arg)) =>
ZipWithSym2KindInference
type instance Apply (ZipWithSym2 l l) l = ZipWithSym3 l l l
instance SuppressUnusedWarnings ZipWithSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) ZipWithSym1KindInference GHC.Tuple.())
data ZipWithSym1 (l :: TyFun a (TyFun b c -> *) -> *)
(l :: TyFun (GHC.Types.[] a) (TyFun (GHC.Types.[] b) (GHC.Types.[] c)
-> *))
= forall arg. (GHC.Types.~) (KindOf (Apply (ZipWithSym1 l) arg)) (KindOf (ZipWithSym2 l arg)) =>
ZipWithSym1KindInference
type instance Apply (ZipWithSym1 l) l = ZipWithSym2 l l
instance SuppressUnusedWarnings ZipWithSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) ZipWithSym0KindInference GHC.Tuple.())
data ZipWithSym0 (l :: TyFun (TyFun a (TyFun b c -> *)
-> *) (TyFun (GHC.Types.[] a) (TyFun (GHC.Types.[] b) (GHC.Types.[] c)
-> *)
-> *))
= forall arg. (GHC.Types.~) (KindOf (Apply ZipWithSym0 arg)) (KindOf (ZipWithSym1 arg)) =>
ZipWithSym0KindInference
type instance Apply ZipWithSym0 l = ZipWithSym1 l
type SplungeSym2 (t :: GHC.Types.[] Nat) (t :: GHC.Types.[] Bool) =
Splunge t t
instance SuppressUnusedWarnings SplungeSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) SplungeSym1KindInference GHC.Tuple.())
data SplungeSym1 (l :: GHC.Types.[] Nat)
(l :: TyFun (GHC.Types.[] Bool) (GHC.Types.[] Nat))
= forall arg. (GHC.Types.~) (KindOf (Apply (SplungeSym1 l) arg)) (KindOf (SplungeSym2 l arg)) =>
SplungeSym1KindInference
type instance Apply (SplungeSym1 l) l = SplungeSym2 l l
instance SuppressUnusedWarnings SplungeSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) SplungeSym0KindInference GHC.Tuple.())
data SplungeSym0 (l :: TyFun (GHC.Types.[] Nat) (TyFun (GHC.Types.[] Bool) (GHC.Types.[] Nat)
-> *))
= forall arg. (GHC.Types.~) (KindOf (Apply SplungeSym0 arg)) (KindOf (SplungeSym1 arg)) =>
SplungeSym0KindInference
type instance Apply SplungeSym0 l = SplungeSym1 l
type EtadSym2 (t :: GHC.Types.[] Nat) (t :: GHC.Types.[] Bool) =
Etad t t
instance SuppressUnusedWarnings EtadSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) EtadSym1KindInference GHC.Tuple.())
data EtadSym1 (l :: GHC.Types.[] Nat)
(l :: TyFun (GHC.Types.[] Bool) (GHC.Types.[] Nat))
= forall arg. (GHC.Types.~) (KindOf (Apply (EtadSym1 l) arg)) (KindOf (EtadSym2 l arg)) =>
EtadSym1KindInference
type instance Apply (EtadSym1 l) l = EtadSym2 l l
instance SuppressUnusedWarnings EtadSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) EtadSym0KindInference GHC.Tuple.())
data EtadSym0 (l :: TyFun (GHC.Types.[] Nat) (TyFun (GHC.Types.[] Bool) (GHC.Types.[] Nat)
-> *))
= forall arg. (GHC.Types.~) (KindOf (Apply EtadSym0 arg)) (KindOf (EtadSym1 arg)) =>
EtadSym0KindInference
type instance Apply EtadSym0 l = EtadSym1 l
type LiftMaybeSym2 (t :: TyFun a b -> *) (t :: Maybe a) =
LiftMaybe t t
instance SuppressUnusedWarnings LiftMaybeSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) LiftMaybeSym1KindInference GHC.Tuple.())
data LiftMaybeSym1 (l :: TyFun a b -> *)
(l :: TyFun (Maybe a) (Maybe b))
= forall arg. (GHC.Types.~) (KindOf (Apply (LiftMaybeSym1 l) arg)) (KindOf (LiftMaybeSym2 l arg)) =>
LiftMaybeSym1KindInference
type instance Apply (LiftMaybeSym1 l) l = LiftMaybeSym2 l l
instance SuppressUnusedWarnings LiftMaybeSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) LiftMaybeSym0KindInference GHC.Tuple.())
data LiftMaybeSym0 (l :: TyFun (TyFun a b
-> *) (TyFun (Maybe a) (Maybe b) -> *))
= forall arg. (GHC.Types.~) (KindOf (Apply LiftMaybeSym0 arg)) (KindOf (LiftMaybeSym1 arg)) =>
LiftMaybeSym0KindInference
type instance Apply LiftMaybeSym0 l = LiftMaybeSym1 l
type MapSym2 (t :: TyFun a b -> *) (t :: GHC.Types.[] a) = Map t t
instance SuppressUnusedWarnings MapSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) MapSym1KindInference GHC.Tuple.())
data MapSym1 (l :: TyFun a b -> *)
(l :: TyFun (GHC.Types.[] a) (GHC.Types.[] b))
= forall arg. (GHC.Types.~) (KindOf (Apply (MapSym1 l) arg)) (KindOf (MapSym2 l arg)) =>
MapSym1KindInference
type instance Apply (MapSym1 l) l = MapSym2 l l
instance SuppressUnusedWarnings MapSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) MapSym0KindInference GHC.Tuple.())
data MapSym0 (l :: TyFun (TyFun a b
-> *) (TyFun (GHC.Types.[] a) (GHC.Types.[] b) -> *))
= forall arg. (GHC.Types.~) (KindOf (Apply MapSym0 arg)) (KindOf (MapSym1 arg)) =>
MapSym0KindInference
type instance Apply MapSym0 l = MapSym1 l
type family Foo (a :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
(a :: TyFun a b -> *)
(a :: a) :: b where
Foo f g a = Apply (Apply f g) a
type family ZipWith (a :: TyFun a (TyFun b c -> *) -> *)
(a :: GHC.Types.[] a)
(a :: GHC.Types.[] b) :: GHC.Types.[] c where
ZipWith f ((GHC.Types.:) x xs) ((GHC.Types.:) y ys) = Apply (Apply (:$) (Apply (Apply f x) y)) (Apply (Apply (Apply ZipWithSym0 f) xs) ys)
ZipWith z GHC.Types.[] GHC.Types.[] = GHC.Types.[]
ZipWith z ((GHC.Types.:) z z) GHC.Types.[] = GHC.Types.[]
ZipWith z GHC.Types.[] ((GHC.Types.:) z z) = GHC.Types.[]
type family Splunge (a :: GHC.Types.[] Nat)
(a :: GHC.Types.[] Bool) :: GHC.Types.[] Nat where
Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789Sym0 ns) bs)) ns) bs
type family Etad (a :: GHC.Types.[] Nat)
(a :: GHC.Types.[] Bool) :: GHC.Types.[] Nat where
Etad a_0123456789 a_0123456789 = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789)) a_0123456789) a_0123456789
type family LiftMaybe (a :: TyFun a b -> *)
(a :: Maybe a) :: Maybe b where
LiftMaybe f (Just x) = Apply JustSym0 (Apply f x)
LiftMaybe z Nothing = NothingSym0
type family Map (a :: TyFun a b -> *)
(a :: GHC.Types.[] a) :: GHC.Types.[] b where
Map z GHC.Types.[] = GHC.Types.[]
Map f ((GHC.Types.:) h t) = Apply (Apply (:$) (Apply f h)) (Apply (Apply MapSym0 f) t)
sFoo ::
forall (t :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *)
(t :: TyFun a b -> *)
(t :: a).
Sing t
-> Sing t -> Sing t -> Sing (Apply (Apply (Apply FooSym0 t) t) t)
sZipWith ::
forall (t :: TyFun a (TyFun b c -> *) -> *)
(t :: GHC.Types.[] a)
(t :: GHC.Types.[] b).
Sing t
-> Sing t
-> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t)
sSplunge ::
forall (t :: GHC.Types.[] Nat) (t :: GHC.Types.[] Bool).
Sing t -> Sing t -> Sing (Apply (Apply SplungeSym0 t) t)
sEtad ::
forall (t :: GHC.Types.[] Nat) (t :: GHC.Types.[] Bool).
Sing t -> Sing t -> Sing (Apply (Apply EtadSym0 t) t)
sLiftMaybe ::
forall (t :: TyFun a b -> *) (t :: Maybe a).
Sing t -> Sing t -> Sing (Apply (Apply LiftMaybeSym0 t) t)
sMap ::
forall (t :: TyFun a b -> *) (t :: GHC.Types.[] a).
Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t)
sFoo sF sG sA
= let
lambda ::
forall f g a. ((GHC.Types.~) t f,
(GHC.Types.~) t g,
(GHC.Types.~) t a) =>
Sing f
-> Sing g -> Sing a -> Sing (Apply (Apply (Apply FooSym0 f) g) a)
lambda f g a = applySing (applySing f g) a
in lambda sF sG sA
sZipWith sF (SCons sX sXs) (SCons sY sYs)
= let
lambda ::
forall f x xs y ys. ((GHC.Types.~) t f,
(GHC.Types.~) t (Apply (Apply (:$) x) xs),
(GHC.Types.~) t (Apply (Apply (:$) y) ys)) =>
Sing f
-> Sing x
-> Sing xs
-> Sing y
-> Sing ys
-> Sing (Apply (Apply (Apply ZipWithSym0 f) (Apply (Apply (:$) x) xs)) (Apply (Apply (:$) y) ys))
lambda f x xs y ys
= applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing (applySing f x) y))
(applySing
(applySing
(applySing (singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith) f) xs)
ys)
in lambda sF sX sXs sY sYs
sZipWith _ SNil SNil
= let
lambda ::
forall wild. ((GHC.Types.~) t wild,
(GHC.Types.~) t GHC.Types.[],
(GHC.Types.~) t GHC.Types.[]) =>
Sing (Apply (Apply (Apply ZipWithSym0 wild) GHC.Types.[]) GHC.Types.[])
lambda = SNil
in lambda
sZipWith _ (SCons _ _) SNil
= let
lambda ::
forall wild wild wild. ((GHC.Types.~) t wild,
(GHC.Types.~) t (Apply (Apply (:$) wild) wild),
(GHC.Types.~) t GHC.Types.[]) =>
Sing (Apply (Apply (Apply ZipWithSym0 wild) (Apply (Apply (:$) wild) wild)) GHC.Types.[])
lambda = SNil
in lambda
sZipWith _ SNil (SCons _ _)
= let
lambda ::
forall wild wild wild. ((GHC.Types.~) t wild,
(GHC.Types.~) t GHC.Types.[],
(GHC.Types.~) t (Apply (Apply (:$) wild) wild)) =>
Sing (Apply (Apply (Apply ZipWithSym0 wild) GHC.Types.[]) (Apply (Apply (:$) wild) wild))
lambda = SNil
in lambda
sSplunge sNs sBs
= let
lambda ::
forall ns bs. ((GHC.Types.~) t ns, (GHC.Types.~) t bs) =>
Sing ns -> Sing bs -> Sing (Apply (Apply SplungeSym0 ns) bs)
lambda ns bs
= applySing
(applySing
(applySing
(singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith)
(singFun2
(Proxy :: Proxy (Apply (Apply Lambda_0123456789Sym0 ns) bs))
(\ sN sB
-> let
lambda ::
forall n b.
Sing n
-> Sing b
-> Sing (Apply (Apply (Apply (Apply Lambda_0123456789Sym0 ns) bs) n) b)
lambda n b
= let
sScrutinee_0123456789 ::
Sing (Let_0123456789Scrutinee_0123456789Sym4 ns bs n b)
sScrutinee_0123456789 = b
in
case sScrutinee_0123456789 of {
STrue
-> let
lambda :: Sing (Case_0123456789 ns bs n b TrueSym0)
lambda
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
n)
in lambda
SFalse
-> let
lambda :: Sing (Case_0123456789 ns bs n b FalseSym0)
lambda = n
in lambda }
in lambda sN sB)))
ns)
bs
in lambda sNs sBs
sEtad sA_0123456789 sA_0123456789
= let
lambda ::
forall a_0123456789 a_0123456789. ((GHC.Types.~) t a_0123456789,
(GHC.Types.~) t a_0123456789) =>
Sing a_0123456789
-> Sing a_0123456789
-> Sing (Apply (Apply EtadSym0 a_0123456789) a_0123456789)
lambda a_0123456789 a_0123456789
= applySing
(applySing
(applySing
(singFun3 (Proxy :: Proxy ZipWithSym0) sZipWith)
(singFun2
(Proxy ::
Proxy (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789))
(\ sN sB
-> let
lambda ::
forall n b.
Sing n
-> Sing b
-> Sing (Apply (Apply (Apply (Apply Lambda_0123456789Sym0 a_0123456789) a_0123456789) n) b)
lambda n b
= let
sScrutinee_0123456789 ::
Sing (Let_0123456789Scrutinee_0123456789Sym4 n b a_0123456789 a_0123456789)
sScrutinee_0123456789 = b
in
case sScrutinee_0123456789 of {
STrue
-> let
lambda ::
Sing (Case_0123456789 n b a_0123456789 a_0123456789 TrueSym0)
lambda
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
n)
in lambda
SFalse
-> let
lambda ::
Sing (Case_0123456789 n b a_0123456789 a_0123456789 FalseSym0)
lambda = n
in lambda }
in lambda sN sB)))
a_0123456789)
a_0123456789
in lambda sA_0123456789 sA_0123456789
sLiftMaybe sF (SJust sX)
= let
lambda ::
forall f x. ((GHC.Types.~) t f,
(GHC.Types.~) t (Apply JustSym0 x)) =>
Sing f
-> Sing x
-> Sing (Apply (Apply LiftMaybeSym0 f) (Apply JustSym0 x))
lambda f x
= applySing
(singFun1 (Proxy :: Proxy JustSym0) SJust) (applySing f x)
in lambda sF sX
sLiftMaybe _ SNothing
= let
lambda ::
forall wild. ((GHC.Types.~) t wild, (GHC.Types.~) t NothingSym0) =>
Sing (Apply (Apply LiftMaybeSym0 wild) NothingSym0)
lambda = SNothing
in lambda
sMap _ SNil
= let
lambda ::
forall wild. ((GHC.Types.~) t wild,
(GHC.Types.~) t GHC.Types.[]) =>
Sing (Apply (Apply MapSym0 wild) GHC.Types.[])
lambda = SNil
in lambda
sMap sF (SCons sH sT)
= let
lambda ::
forall f h t. ((GHC.Types.~) t f,
(GHC.Types.~) t (Apply (Apply (:$) h) t)) =>
Sing f
-> Sing h
-> Sing t
-> Sing (Apply (Apply MapSym0 f) (Apply (Apply (:$) h) t))
lambda f h t
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) (applySing f h))
(applySing
(applySing (singFun2 (Proxy :: Proxy MapSym0) sMap) f) t)
in lambda sF sH sT
data instance Sing (z :: Either a b)
= forall (n :: a). (GHC.Types.~) z (Left n) => SLeft (Sing n) |
forall (n :: b). (GHC.Types.~) z (Right n) => SRight (Sing n)
type SEither (z :: Either a b) = Sing z
instance (SingKind (KProxy :: KProxy a),
SingKind (KProxy :: KProxy b)) =>
SingKind (KProxy :: KProxy (Either a b)) where
type DemoteRep (KProxy :: KProxy (Either a b)) = Either (DemoteRep (KProxy :: KProxy a)) (DemoteRep (KProxy :: KProxy b))
fromSing (SLeft b) = Left (fromSing b)
fromSing (SRight b) = Right (fromSing b)
toSing (Left b)
= case toSing b :: SomeSing (KProxy :: KProxy a) of {
SomeSing c -> SomeSing (SLeft c) }
toSing (Right b)
= case toSing b :: SomeSing (KProxy :: KProxy b) of {
SomeSing c -> SomeSing (SRight c) }
instance SingI n => SingI (Left (n :: a)) where
sing = SLeft sing
instance SingI n => SingI (Right (n :: b)) where
sing = SRight sing