singletons-base-3.5: 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 LamCases_0123456789876543210 (xs0123456789876543210 :: [Bool]) a_0123456789876543210 where
LamCases_0123456789876543210 xs x = Apply (Apply (>>@#@$) (Apply GuardSym0 x)) (Apply ReturnSym0 x)
data LamCases_0123456789876543210Sym0 (xs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 xs0123456789876543210) arg) (LamCases_0123456789876543210Sym1 xs0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 xs0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 xs0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 xs0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (xs0123456789876543210 :: [Bool]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 xs0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_0123456789876543210 where
LamCases_0123456789876543210 x xs ys y = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y)
data LamCases_0123456789876543210Sym0 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_0123456789876543210 where
LamCases_0123456789876543210 xs ys x = Apply (Apply (>>=@#@$) ys) (LamCases_0123456789876543210Sym0 x xs ys)
data LamCases_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_0123456789876543210 where
LamCases_0123456789876543210 xs ys x = Apply ReturnSym0 x
data LamCases_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_0123456789876543210 where
LamCases_0123456789876543210 xs ys y = Apply ReturnSym0 y
data LamCases_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_0123456789876543210 where
LamCases_0123456789876543210 xs ys '(x,
y) = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y)
data LamCases_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 xs0123456789876543210 ys0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_0123456789876543210 where
LamCases_0123456789876543210 a ma mb b = Apply (Apply (>>@#@$) (Apply GuardSym0 b)) (Apply ReturnSym0 a)
data LamCases_0123456789876543210Sym0 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) arg) (LamCases_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_0123456789876543210 where
LamCases_0123456789876543210 ma mb a = Apply (Apply (>>=@#@$) mb) (LamCases_0123456789876543210Sym0 a ma mb)
data LamCases_0123456789876543210Sym0 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210) arg) (LamCases_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a_01234567898765432100123456789876543210
type TruesSym0 :: (~>) [Bool] [Bool]
data TruesSym0 :: (~>) [Bool] [Bool]
where
TruesSym0KindInference :: SameKind (Apply TruesSym0 arg) (TruesSym1 arg) =>
TruesSym0 a0123456789876543210
type instance Apply @[Bool] @[Bool] TruesSym0 a0123456789876543210 = Trues a0123456789876543210
instance SuppressUnusedWarnings TruesSym0 where
suppressUnusedWarnings = snd ((,) TruesSym0KindInference ())
type TruesSym1 :: [Bool] -> [Bool]
type family TruesSym1 (a0123456789876543210 :: [Bool]) :: [Bool] where
TruesSym1 a0123456789876543210 = Trues a0123456789876543210
type CartProdSym0 :: (~>) [a] ((~>) [b] [(a, b)])
data CartProdSym0 :: (~>) [a] ((~>) [b] [(a, b)])
where
CartProdSym0KindInference :: SameKind (Apply CartProdSym0 arg) (CartProdSym1 arg) =>
CartProdSym0 a0123456789876543210
type instance Apply @[a] @((~>) [b] [(a,
b)]) CartProdSym0 a0123456789876543210 = CartProdSym1 a0123456789876543210
instance SuppressUnusedWarnings CartProdSym0 where
suppressUnusedWarnings = snd ((,) CartProdSym0KindInference ())
type CartProdSym1 :: [a] -> (~>) [b] [(a, b)]
data CartProdSym1 (a0123456789876543210 :: [a]) :: (~>) [b] [(a,
b)]
where
CartProdSym1KindInference :: SameKind (Apply (CartProdSym1 a0123456789876543210) arg) (CartProdSym2 a0123456789876543210 arg) =>
CartProdSym1 a0123456789876543210 a0123456789876543210
type instance Apply @[b] @[(a,
b)] (CartProdSym1 a0123456789876543210) a0123456789876543210 = CartProd a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (CartProdSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) CartProdSym1KindInference ())
type CartProdSym2 :: [a] -> [b] -> [(a, b)]
type family CartProdSym2 @a @b (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a,
b)] where
CartProdSym2 a0123456789876543210 a0123456789876543210 = CartProd a0123456789876543210 a0123456789876543210
type Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)])
data Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)])
where
Zip'Sym0KindInference :: SameKind (Apply Zip'Sym0 arg) (Zip'Sym1 arg) =>
Zip'Sym0 a0123456789876543210
type instance Apply @[a] @((~>) [b] [(a,
b)]) 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 :: [a]) :: (~>) [b] [(a, b)]
where
Zip'Sym1KindInference :: SameKind (Apply (Zip'Sym1 a0123456789876543210) arg) (Zip'Sym2 a0123456789876543210 arg) =>
Zip'Sym1 a0123456789876543210 a0123456789876543210
type instance Apply @[b] @[(a,
b)] (Zip'Sym1 a0123456789876543210) a0123456789876543210 = Zip' a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Zip'Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) Zip'Sym1KindInference ())
type Zip'Sym2 :: [a] -> [b] -> [(a, b)]
type family Zip'Sym2 @a @b (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a,
b)] where
Zip'Sym2 a0123456789876543210 a0123456789876543210 = Zip' a0123456789876543210 a0123456789876543210
type BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a))
data BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a))
where
BoogieSym0KindInference :: SameKind (Apply BoogieSym0 arg) (BoogieSym1 arg) =>
BoogieSym0 a0123456789876543210
type instance Apply @(Maybe a) @((~>) (Maybe Bool) (Maybe a)) BoogieSym0 a0123456789876543210 = BoogieSym1 a0123456789876543210
instance SuppressUnusedWarnings BoogieSym0 where
suppressUnusedWarnings = snd ((,) BoogieSym0KindInference ())
type BoogieSym1 :: Maybe a -> (~>) (Maybe Bool) (Maybe a)
data BoogieSym1 (a0123456789876543210 :: Maybe a) :: (~>) (Maybe Bool) (Maybe a)
where
BoogieSym1KindInference :: SameKind (Apply (BoogieSym1 a0123456789876543210) arg) (BoogieSym2 a0123456789876543210 arg) =>
BoogieSym1 a0123456789876543210 a0123456789876543210
type instance Apply @(Maybe Bool) @(Maybe a) (BoogieSym1 a0123456789876543210) a0123456789876543210 = Boogie a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BoogieSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) BoogieSym1KindInference ())
type BoogieSym2 :: Maybe a -> Maybe Bool -> Maybe a
type family BoogieSym2 @a (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe Bool) :: Maybe a where
BoogieSym2 a0123456789876543210 a0123456789876543210 = Boogie a0123456789876543210 a0123456789876543210
type Trues :: [Bool] -> [Bool]
type family Trues (a :: [Bool]) :: [Bool] where
Trues xs = Apply (Apply (>>=@#@$) xs) (LamCases_0123456789876543210Sym0 xs)
type CartProd :: [a] -> [b] -> [(a, b)]
type family CartProd @a @b (a :: [a]) (a :: [b]) :: [(a, b)] where
CartProd xs ys = Apply (Apply (>>=@#@$) xs) (LamCases_0123456789876543210Sym0 xs ys)
type Zip' :: [a] -> [b] -> [(a, b)]
type family Zip' @a @b (a :: [a]) (a :: [b]) :: [(a, b)] where
Zip' xs ys = Apply (Apply (>>=@#@$) (Apply (Apply MzipSym0 (Apply (Apply (>>=@#@$) xs) (LamCases_0123456789876543210Sym0 xs ys))) (Apply (Apply (>>=@#@$) ys) (LamCases_0123456789876543210Sym0 xs ys)))) (LamCases_0123456789876543210Sym0 xs ys)
type Boogie :: Maybe a -> Maybe Bool -> Maybe a
type family Boogie @a (a :: Maybe a) (a :: Maybe Bool) :: Maybe a where
Boogie ma mb = Apply (Apply (>>=@#@$) ma) (LamCases_0123456789876543210Sym0 ma mb)
sTrues ::
(forall (t :: [Bool]). Sing t -> Sing (Trues t :: [Bool]) :: Type)
sCartProd ::
(forall (t :: [a]) (t :: [b]).
Sing t -> Sing t -> Sing (CartProd t t :: [(a, b)]) :: Type)
sZip' ::
(forall (t :: [a]) (t :: [b]).
Sing t -> Sing t -> Sing (Zip' t t :: [(a, b)]) :: Type)
sBoogie ::
(forall (t :: Maybe a) (t :: Maybe Bool).
Sing t -> Sing t -> Sing (Boogie t t :: Maybe a) :: Type)
sTrues (sXs :: Sing xs)
= applySing
(applySing (singFun2 @(>>=@#@$) (%>>=)) sXs)
(singFun1
@(LamCases_0123456789876543210Sym0 xs)
(\cases
(sX :: 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
@(LamCases_0123456789876543210Sym0 xs ys)
(\cases
(sX :: Sing x)
-> applySing
(applySing (singFun2 @(>>=@#@$) (%>>=)) sYs)
(singFun1
@(LamCases_0123456789876543210Sym0 x xs ys)
(\cases
(sY :: 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
@(LamCases_0123456789876543210Sym0 xs ys)
(\cases
(sX :: Sing x) -> applySing (singFun1 @ReturnSym0 sReturn) sX))))
(applySing
(applySing (singFun2 @(>>=@#@$) (%>>=)) sYs)
(singFun1
@(LamCases_0123456789876543210Sym0 xs ys)
(\cases
(sY :: Sing y) -> applySing (singFun1 @ReturnSym0 sReturn) sY)))))
(singFun1
@(LamCases_0123456789876543210Sym0 xs ys)
(\cases
(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
@(LamCases_0123456789876543210Sym0 ma mb)
(\cases
(sA :: Sing a)
-> applySing
(applySing (singFun2 @(>>=@#@$) (%>>=)) sMb)
(singFun1
@(LamCases_0123456789876543210Sym0 a ma mb)
(\cases
(sB :: 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 SingI1 (CartProdSym1 :: [a] -> (~>) [b] [(a, b)]) where
liftSing (s :: Sing (d :: [a]))
= singFun1 @(CartProdSym1 (d :: [a])) (sCartProd s)
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 SingI1 (Zip'Sym1 :: [a] -> (~>) [b] [(a, b)]) where
liftSing (s :: Sing (d :: [a]))
= singFun1 @(Zip'Sym1 (d :: [a])) (sZip' s)
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))
instance SingI1 (BoogieSym1 :: Maybe a
-> (~>) (Maybe Bool) (Maybe a)) where
liftSing (s :: Sing (d :: Maybe a))
= singFun1 @(BoogieSym1 (d :: Maybe a)) (sBoogie s)