singletons-2.7: tests/compile-and-dump/Singletons/T184.golden
Singletons/T184.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| boogie :: Maybe a -> Maybe Bool -> Maybe a
boogie ma mb
= do a <- ma
b <- mb
guard b
return a
zip' :: [a] -> [b] -> [(a, b)]
zip' xs ys = [(x, y) | x <- xs | y <- ys]
cartProd :: [a] -> [b] -> [(a, b)]
cartProd xs ys = [(x, y) | x <- xs, y <- ys]
trues :: [Bool] -> [Bool]
trues xs = [x | x <- xs, x] |]
======>
boogie :: Maybe a -> Maybe Bool -> Maybe a
boogie ma mb
= do a <- ma
b <- mb
guard b
return a
zip' :: [a] -> [b] -> [(a, b)]
zip' xs ys = [(x, y) | x <- xs | y <- ys]
cartProd :: [a] -> [b] -> [(a, b)]
cartProd xs ys = [(x, y) | x <- xs, y <- ys]
trues :: [Bool] -> [Bool]
trues xs = [x | x <- xs, x]
type family Lambda_0123456789876543210 xs x where
Lambda_0123456789876543210 xs x = Apply (Apply (>>@#@$) (Apply GuardSym0 x)) (Apply ReturnSym0 x)
data Lambda_0123456789876543210Sym0 xs0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 xs0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 xs0123456789876543210 = Lambda_0123456789876543210Sym1 xs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 xs0123456789876543210 x0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym2 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 xs0123456789876543210 x0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
type Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210 =
Lambda_0123456789876543210 xs0123456789876543210 x0123456789876543210
type family Lambda_0123456789876543210 x xs ys y where
Lambda_0123456789876543210 x xs ys y = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y)
data Lambda_0123456789876543210Sym0 x0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 x0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 x0123456789876543210 = Lambda_0123456789876543210Sym1 x0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) xs0123456789876543210 = Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210 ys0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210 ys0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210) ys0123456789876543210 = Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 x0123456789876543210 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
data Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
where
Lambda_0123456789876543210Sym3KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg) =>
Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) y0123456789876543210 = Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym3KindInference) ())
type Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 =
Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
type family Lambda_0123456789876543210 xs ys x where
Lambda_0123456789876543210 xs ys x = Apply (Apply (>>=@#@$) ys) (Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) xs) ys)
data Lambda_0123456789876543210Sym0 xs0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 xs0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 xs0123456789876543210 = Lambda_0123456789876543210Sym1 xs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym2 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) ys0123456789876543210 = Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
type Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 =
Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
type family Lambda_0123456789876543210 xs ys x where
Lambda_0123456789876543210 xs ys x = Apply ReturnSym0 x
data Lambda_0123456789876543210Sym0 xs0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 xs0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 xs0123456789876543210 = Lambda_0123456789876543210Sym1 xs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym2 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) ys0123456789876543210 = Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
type Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 =
Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210
type family Lambda_0123456789876543210 xs ys y where
Lambda_0123456789876543210 xs ys y = Apply ReturnSym0 y
data Lambda_0123456789876543210Sym0 xs0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 xs0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 xs0123456789876543210 = Lambda_0123456789876543210Sym1 xs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym2 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) ys0123456789876543210 = Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) y0123456789876543210 = Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
type Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 =
Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210
type family Case_0123456789876543210 arg_0123456789876543210 xs ys t where
Case_0123456789876543210 arg_0123456789876543210 xs ys '(x,
y) = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y)
type family Lambda_0123456789876543210 xs ys arg_0123456789876543210 where
Lambda_0123456789876543210 xs ys arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 xs ys arg_0123456789876543210
data Lambda_0123456789876543210Sym0 xs0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 xs0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 xs0123456789876543210 = Lambda_0123456789876543210Sym1 xs0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym2 xs0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 xs0123456789876543210) ys0123456789876543210 = Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
type Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 =
Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210
type family Lambda_0123456789876543210 a ma mb b where
Lambda_0123456789876543210 a ma mb b = Apply (Apply (>>@#@$) (Apply GuardSym0 b)) (Apply ReturnSym0 a)
data Lambda_0123456789876543210Sym0 a0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 a0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 a0123456789876543210 = Lambda_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a0123456789876543210) arg) (Lambda_0123456789876543210Sym2 a0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 a0123456789876543210) ma0123456789876543210 = Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210 mb0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210) arg) (Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210 mb0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210) mb0123456789876543210 = Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 a0123456789876543210 ma0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
data Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210
where
Lambda_0123456789876543210Sym3KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) arg) (Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 arg) =>
Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) b0123456789876543210 = Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym3KindInference) ())
type Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 =
Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210
type family Lambda_0123456789876543210 ma mb a where
Lambda_0123456789876543210 ma mb a = Apply (Apply (>>=@#@$) mb) (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) ma) mb)
data Lambda_0123456789876543210Sym0 ma0123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 ma0123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 ma0123456789876543210 = Lambda_0123456789876543210Sym1 ma0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 ma0123456789876543210) arg) (Lambda_0123456789876543210Sym2 ma0123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 ma0123456789876543210) mb0123456789876543210 = Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 ma0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210 a0123456789876543210
where
Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210) arg) (Lambda_0123456789876543210Sym3 ma0123456789876543210 mb0123456789876543210 arg) =>
Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210 a0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210) a0123456789876543210 = Lambda_0123456789876543210Sym3 ma0123456789876543210 mb0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym2KindInference) ())
type Lambda_0123456789876543210Sym3 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 =
Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a0123456789876543210
type TruesSym0 :: (~>) [Bool] [Bool]
data TruesSym0 a0123456789876543210
where
TruesSym0KindInference :: SameKind (Apply TruesSym0 arg) (TruesSym1 arg) =>
TruesSym0 a0123456789876543210
type instance Apply TruesSym0 a0123456789876543210 = TruesSym1 a0123456789876543210
instance SuppressUnusedWarnings TruesSym0 where
suppressUnusedWarnings = snd (((,) TruesSym0KindInference) ())
type TruesSym1 (a0123456789876543210 :: [Bool]) =
Trues a0123456789876543210 :: [Bool]
type CartProdSym0 :: (~>) [a] ((~>) [b] [(a, b)])
data CartProdSym0 a0123456789876543210
where
CartProdSym0KindInference :: SameKind (Apply CartProdSym0 arg) (CartProdSym1 arg) =>
CartProdSym0 a0123456789876543210
type instance Apply CartProdSym0 a0123456789876543210 = CartProdSym1 a0123456789876543210
instance SuppressUnusedWarnings CartProdSym0 where
suppressUnusedWarnings = snd (((,) CartProdSym0KindInference) ())
type CartProdSym1 :: [a] -> (~>) [b] [(a, b)]
data CartProdSym1 a0123456789876543210 a0123456789876543210
where
CartProdSym1KindInference :: SameKind (Apply (CartProdSym1 a0123456789876543210) arg) (CartProdSym2 a0123456789876543210 arg) =>
CartProdSym1 a0123456789876543210 a0123456789876543210
type instance Apply (CartProdSym1 a0123456789876543210) a0123456789876543210 = CartProdSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (CartProdSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) CartProdSym1KindInference) ())
type CartProdSym2 (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) =
CartProd a0123456789876543210 a0123456789876543210 :: [(a, b)]
type Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)])
data Zip'Sym0 a0123456789876543210
where
Zip'Sym0KindInference :: SameKind (Apply Zip'Sym0 arg) (Zip'Sym1 arg) =>
Zip'Sym0 a0123456789876543210
type instance Apply Zip'Sym0 a0123456789876543210 = Zip'Sym1 a0123456789876543210
instance SuppressUnusedWarnings Zip'Sym0 where
suppressUnusedWarnings = snd (((,) Zip'Sym0KindInference) ())
type Zip'Sym1 :: [a] -> (~>) [b] [(a, b)]
data Zip'Sym1 a0123456789876543210 a0123456789876543210
where
Zip'Sym1KindInference :: SameKind (Apply (Zip'Sym1 a0123456789876543210) arg) (Zip'Sym2 a0123456789876543210 arg) =>
Zip'Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Zip'Sym1 a0123456789876543210) a0123456789876543210 = Zip'Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Zip'Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) Zip'Sym1KindInference) ())
type Zip'Sym2 (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) =
Zip' a0123456789876543210 a0123456789876543210 :: [(a, b)]
type BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a))
data BoogieSym0 a0123456789876543210
where
BoogieSym0KindInference :: SameKind (Apply BoogieSym0 arg) (BoogieSym1 arg) =>
BoogieSym0 a0123456789876543210
type instance Apply BoogieSym0 a0123456789876543210 = BoogieSym1 a0123456789876543210
instance SuppressUnusedWarnings BoogieSym0 where
suppressUnusedWarnings = snd (((,) BoogieSym0KindInference) ())
type BoogieSym1 :: Maybe a -> (~>) (Maybe Bool) (Maybe a)
data BoogieSym1 a0123456789876543210 a0123456789876543210
where
BoogieSym1KindInference :: SameKind (Apply (BoogieSym1 a0123456789876543210) arg) (BoogieSym2 a0123456789876543210 arg) =>
BoogieSym1 a0123456789876543210 a0123456789876543210
type instance Apply (BoogieSym1 a0123456789876543210) a0123456789876543210 = BoogieSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BoogieSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) BoogieSym1KindInference) ())
type BoogieSym2 (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe Bool) =
Boogie a0123456789876543210 a0123456789876543210 :: Maybe a
type Trues :: [Bool] -> [Bool]
type family Trues a where
Trues xs = Apply (Apply (>>=@#@$) xs) (Apply Lambda_0123456789876543210Sym0 xs)
type CartProd :: [a] -> [b] -> [(a, b)]
type family CartProd a a where
CartProd xs ys = Apply (Apply (>>=@#@$) xs) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys)
type Zip' :: [a] -> [b] -> [(a, b)]
type family Zip' a a where
Zip' xs ys = Apply (Apply (>>=@#@$) (Apply (Apply MzipSym0 (Apply (Apply (>>=@#@$) xs) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))) (Apply (Apply (>>=@#@$) ys) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys)))) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys)
type Boogie :: Maybe a -> Maybe Bool -> Maybe a
type family Boogie a a where
Boogie ma mb = Apply (Apply (>>=@#@$) ma) (Apply (Apply Lambda_0123456789876543210Sym0 ma) mb)
sTrues ::
forall (t :: [Bool]). Sing t -> Sing (Apply TruesSym0 t :: [Bool])
sCartProd ::
forall a b (t :: [a]) (t :: [b]).
Sing t
-> Sing t -> Sing (Apply (Apply CartProdSym0 t) t :: [(a, b)])
sZip' ::
forall a b (t :: [a]) (t :: [b]).
Sing t -> Sing t -> Sing (Apply (Apply Zip'Sym0 t) t :: [(a, b)])
sBoogie ::
forall a (t :: Maybe a) (t :: Maybe Bool).
Sing t -> Sing t -> Sing (Apply (Apply BoogieSym0 t) t :: Maybe a)
sTrues (sXs :: Sing xs)
= (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sXs))
((singFun1 @(Apply Lambda_0123456789876543210Sym0 xs))
(\ sX
-> case sX of {
(_ :: Sing x)
-> (applySing
((applySing ((singFun2 @(>>@#@$)) (%>>)))
((applySing ((singFun1 @GuardSym0) sGuard)) sX)))
((applySing ((singFun1 @ReturnSym0) sReturn)) sX) }))
sCartProd (sXs :: Sing xs) (sYs :: Sing ys)
= (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sXs))
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))
(\ sX
-> case sX of {
(_ :: Sing x)
-> (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sYs))
((singFun1
@(Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) xs) ys))
(\ sY
-> case sY of {
(_ :: Sing y)
-> (applySing ((singFun1 @ReturnSym0) sReturn))
((applySing
((applySing ((singFun2 @Tuple2Sym0) STuple2)) sX))
sY) })) }))
sZip' (sXs :: Sing xs) (sYs :: Sing ys)
= (applySing
((applySing ((singFun2 @(>>=@#@$)) (%>>=)))
((applySing
((applySing ((singFun2 @MzipSym0) sMzip))
((applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sXs))
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))
(\ sX
-> case sX of {
(_ :: Sing x)
-> (applySing ((singFun1 @ReturnSym0) sReturn)) sX })))))
((applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sYs))
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))
(\ sY
-> case sY of {
(_ :: Sing y)
-> (applySing ((singFun1 @ReturnSym0) sReturn)) sY }))))))
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))
(\ sArg_0123456789876543210
-> case sArg_0123456789876543210 of {
(_ :: Sing arg_0123456789876543210)
-> (id
@(Sing (Case_0123456789876543210 arg_0123456789876543210 xs ys arg_0123456789876543210)))
(case sArg_0123456789876543210 of {
STuple2 (sX :: Sing x) (sY :: Sing y)
-> (applySing ((singFun1 @ReturnSym0) sReturn))
((applySing ((applySing ((singFun2 @Tuple2Sym0) STuple2)) sX))
sY) }) }))
sBoogie (sMa :: Sing ma) (sMb :: Sing mb)
= (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sMa))
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 ma) mb))
(\ sA
-> case sA of {
(_ :: Sing a)
-> (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sMb))
((singFun1
@(Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) ma) mb))
(\ sB
-> case sB of {
(_ :: Sing b)
-> (applySing
((applySing ((singFun2 @(>>@#@$)) (%>>)))
((applySing ((singFun1 @GuardSym0) sGuard)) sB)))
((applySing ((singFun1 @ReturnSym0) sReturn))
sA) })) }))
instance SingI (TruesSym0 :: (~>) [Bool] [Bool]) where
sing = (singFun1 @TruesSym0) sTrues
instance SingI (CartProdSym0 :: (~>) [a] ((~>) [b] [(a, b)])) where
sing = (singFun2 @CartProdSym0) sCartProd
instance SingI d =>
SingI (CartProdSym1 (d :: [a]) :: (~>) [b] [(a, b)]) where
sing = (singFun1 @(CartProdSym1 (d :: [a]))) (sCartProd (sing @d))
instance SingI (Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)])) where
sing = (singFun2 @Zip'Sym0) sZip'
instance SingI d =>
SingI (Zip'Sym1 (d :: [a]) :: (~>) [b] [(a, b)]) where
sing = (singFun1 @(Zip'Sym1 (d :: [a]))) (sZip' (sing @d))
instance SingI (BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a))) where
sing = (singFun2 @BoogieSym0) sBoogie
instance SingI d =>
SingI (BoogieSym1 (d :: Maybe a) :: (~>) (Maybe Bool) (Maybe a)) where
sing = (singFun1 @(BoogieSym1 (d :: Maybe a))) (sBoogie (sing @d))