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 xs0123456789876543210 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_0123456789876543210 xs0123456789876543210 x0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 xs0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) type family Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 x0123456789876543210 type family Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 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_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 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_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 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_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 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_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 xs0123456789876543210 ys0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 xs ys '(x, y) = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y) type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 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_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 type family Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 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_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 type family Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 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_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 ma0123456789876543210 mb0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 where Lambda_0123456789876543210Sym3 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 = Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 type TruesSym0 :: (~>) [Bool] [Bool] data TruesSym0 :: (~>) [Bool] [Bool] where TruesSym0KindInference :: SameKind (Apply TruesSym0 arg) (TruesSym1 arg) => TruesSym0 a0123456789876543210 type instance Apply 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 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 (CartProdSym1 a0123456789876543210) a0123456789876543210 = CartProd a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (CartProdSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CartProdSym1KindInference ()) type CartProdSym2 :: [a] -> [b] -> [(a, b)] type family CartProdSym2 (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 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 (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 (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 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 (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 (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) (Apply Lambda_0123456789876543210Sym0 xs) type CartProd :: [a] -> [b] -> [(a, b)] type family CartProd (a :: [a]) (a :: [b]) :: [(a, b)] where CartProd xs ys = Apply (Apply (>>=@#@$) xs) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys) type Zip' :: [a] -> [b] -> [(a, b)] type family Zip' (a :: [a]) (a :: [b]) :: [(a, b)] 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 :: Maybe a) (a :: Maybe Bool) :: Maybe 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]) :: Type) sCartProd :: (forall (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply CartProdSym0 t) t :: [(a, b)]) :: Type) sZip' :: (forall (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply Zip'Sym0 t) t :: [(a, b)]) :: Type) sBoogie :: (forall (t :: Maybe a) (t :: Maybe Bool). Sing t -> Sing t -> Sing (Apply (Apply BoogieSym0 t) t :: Maybe a) :: Type) 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 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)