{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Foldable'. module Language.Symantic.Compiling.Foldable where import Data.Foldable (Foldable) import qualified Data.Foldable as Foldable import Control.Monad (liftM, liftM2, liftM3) import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (Foldable(..) , all, and, any, concat, concatMap , mapM_, notElem, or, sequence, sequence_) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_Foldable' class Sym_Foldable term where foldMap :: (Foldable f, Monoid m) => term (a -> m) -> term (f a) -> term m foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b length :: Foldable f => term (f a) -> term Int null :: Foldable f => term (f a) -> term Bool minimum :: (Foldable f, Ord a) => term (f a) -> term a maximum :: (Foldable f, Ord a) => term (f a) -> term a elem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool sum :: (Foldable f, Num a) => term (f a) -> term a product :: (Foldable f, Num a) => term (f a) -> term a toList :: Foldable f => term (f a) -> term [a] all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool and :: Foldable f => term (f Bool) -> term Bool any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool concat :: Foldable f => term (f [a]) -> term [a] concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b] find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a) foldlM :: (Foldable f, Monad m) => term (b -> a -> m b) -> term b -> term (f a) -> term (m b) foldrM :: (Foldable f, Monad m) => term (a -> b -> m b) -> term b -> term (f a) -> term (m b) forM_ :: (Foldable f, Monad m) => term (f a) -> term (a -> m b) -> term (m ()) for_ :: (Foldable f, Applicative p) => term (f a) -> term (a -> p b) -> term (p ()) mapM_ :: (Foldable f, Monad m) => term (a -> m b) -> term (f a) -> term (m ()) maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a notElem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool or :: Foldable f => term (f Bool) -> term Bool sequenceA_ :: (Foldable f, Applicative p) => term (f (p a)) -> term (p ()) sequence_ :: (Foldable f, Monad m) => term (f (m a)) -> term (m ()) traverse_ :: (Foldable f, Applicative p) => term (a -> p b) -> term (f a) -> term (p ()) -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a default foldMap :: (Trans t term, Foldable f, Monoid m) => t term (a -> m) -> t term (f a) -> t term m default foldr :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b default foldr' :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b default foldl :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b default foldl' :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b default length :: (Trans t term, Foldable f) => t term (f a) -> t term Int default null :: (Trans t term, Foldable f) => t term (f a) -> t term Bool default minimum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a default maximum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a default elem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool default sum :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a default product :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a default toList :: (Trans t term, Foldable f) => t term (f a) -> t term [a] default all :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool default and :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool default any :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool default concat :: (Trans t term, Foldable f) => t term (f [a]) -> t term [a] default concatMap :: (Trans t term, Foldable f) => t term (a -> [b]) -> t term (f a) -> t term [b] default find :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term (Maybe a) default foldlM :: (Trans t term, Foldable f, Monad m) => t term (b -> a -> m b) -> t term b -> t term (f a) -> t term (m b) default foldrM :: (Trans t term, Foldable f, Monad m) => t term (a -> b -> m b) -> t term b -> t term (f a) -> t term (m b) default forM_ :: (Trans t term, Foldable f, Monad m) => t term (f a) -> t term (a -> m b) -> t term (m ()) default for_ :: (Trans t term, Foldable f, Applicative p) => t term (f a) -> t term (a -> p b) -> t term (p ()) default mapM_ :: (Trans t term, Foldable f, Monad m) => t term (a -> m b) -> t term (f a) -> t term (m ()) default maximumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a default minimumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a default notElem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool default or :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool default sequenceA_ :: (Trans t term, Foldable f, Applicative p) => t term (f (p a)) -> t term (p ()) default sequence_ :: (Trans t term, Foldable f, Monad m) => t term (f (m a)) -> t term (m ()) default traverse_ :: (Trans t term, Foldable f, Applicative p) => t term (a -> p b) -> t term (f a) -> t term (p ()) foldMap = trans_map2 foldMap foldr = trans_map3 foldr foldr' = trans_map3 foldr' foldl = trans_map3 foldl foldl' = trans_map3 foldl' length = trans_map1 length null = trans_map1 null minimum = trans_map1 minimum maximum = trans_map1 maximum elem = trans_map2 elem sum = trans_map1 sum product = trans_map1 product toList = trans_map1 toList all = trans_map2 all and = trans_map1 and any = trans_map2 any concat = trans_map1 concat concatMap = trans_map2 concatMap find = trans_map2 find foldlM = trans_map3 foldlM foldrM = trans_map3 foldrM forM_ = trans_map2 forM_ for_ = trans_map2 for_ mapM_ = trans_map2 mapM_ maximumBy = trans_map2 maximumBy minimumBy = trans_map2 minimumBy notElem = trans_map2 notElem or = trans_map1 or sequenceA_ = trans_map1 sequenceA_ sequence_ = trans_map1 sequence_ traverse_ = trans_map2 traverse_ type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable type instance Consts_of_Iface (Proxy Foldable) = Proxy Foldable ': Consts_imported_by Foldable type instance Consts_imported_by Foldable = '[] instance Sym_Foldable HostI where foldMap = liftM2 Foldable.foldMap foldr = liftM3 Foldable.foldr foldr' = liftM3 Foldable.foldr' foldl = liftM3 Foldable.foldl foldl' = liftM3 Foldable.foldl' null = liftM Foldable.null length = liftM Foldable.length minimum = liftM Foldable.minimum maximum = liftM Foldable.maximum elem = liftM2 Foldable.elem sum = liftM Foldable.sum product = liftM Foldable.product toList = liftM Foldable.toList all = liftM2 Foldable.all and = liftM Foldable.and any = liftM2 Foldable.any concat = liftM Foldable.concat concatMap = liftM2 Foldable.concatMap find = liftM2 Foldable.find foldlM = liftM3 Foldable.foldlM foldrM = liftM3 Foldable.foldrM forM_ = liftM2 Foldable.forM_ for_ = liftM2 Foldable.for_ mapM_ = liftM2 Foldable.mapM_ maximumBy = liftM2 Foldable.maximumBy minimumBy = liftM2 Foldable.minimumBy notElem = liftM2 Foldable.notElem or = liftM Foldable.or sequenceA_ = liftM Foldable.sequenceA_ sequence_ = liftM Foldable.sequence_ traverse_ = liftM2 Foldable.traverse_ instance Sym_Foldable TextI where foldMap = textI2 "foldMap" foldr = textI3 "foldr" foldr' = textI3 "foldr'" foldl = textI3 "foldl" foldl' = textI3 "foldl'" null = textI1 "null" length = textI1 "length" minimum = textI1 "minimum" maximum = textI1 "maximum" elem = textI2 "elem" sum = textI1 "sum" product = textI1 "product" toList = textI1 "toList" all = textI2 "all" and = textI1 "and" any = textI2 "any" concat = textI1 "concat" concatMap = textI2 "concatMap" find = textI2 "find" foldlM = textI3 "foldlM" foldrM = textI3 "foldrM" forM_ = textI2 "forM_" for_ = textI2 "for_" mapM_ = textI2 "mapM_" maximumBy = textI2 "maximumBy" minimumBy = textI2 "minimumBy" notElem = textI2 "notElem" or = textI1 "or" sequenceA_ = textI1 "sequenceA_" sequence_ = textI1 "sequence_" traverse_ = textI2 "traverse_" instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where foldMap = dupI2 (Proxy @Sym_Foldable) foldMap foldr = dupI3 (Proxy @Sym_Foldable) foldr foldr' = dupI3 (Proxy @Sym_Foldable) foldr' foldl = dupI3 (Proxy @Sym_Foldable) foldl foldl' = dupI3 (Proxy @Sym_Foldable) foldl' null = dupI1 (Proxy @Sym_Foldable) null length = dupI1 (Proxy @Sym_Foldable) length minimum = dupI1 (Proxy @Sym_Foldable) minimum maximum = dupI1 (Proxy @Sym_Foldable) maximum elem = dupI2 (Proxy @Sym_Foldable) elem sum = dupI1 (Proxy @Sym_Foldable) sum product = dupI1 (Proxy @Sym_Foldable) product toList = dupI1 (Proxy @Sym_Foldable) toList all = dupI2 (Proxy @Sym_Foldable) all and = dupI1 (Proxy @Sym_Foldable) and any = dupI2 (Proxy @Sym_Foldable) any concat = dupI1 (Proxy @Sym_Foldable) concat concatMap = dupI2 (Proxy @Sym_Foldable) concatMap find = dupI2 (Proxy @Sym_Foldable) find foldlM = dupI3 (Proxy @Sym_Foldable) foldlM foldrM = dupI3 (Proxy @Sym_Foldable) foldrM forM_ = dupI2 (Proxy @Sym_Foldable) forM_ for_ = dupI2 (Proxy @Sym_Foldable) for_ mapM_ = dupI2 (Proxy @Sym_Foldable) mapM_ maximumBy = dupI2 (Proxy @Sym_Foldable) maximumBy minimumBy = dupI2 (Proxy @Sym_Foldable) minimumBy notElem = dupI2 (Proxy @Sym_Foldable) notElem or = dupI1 (Proxy @Sym_Foldable) or sequenceA_ = dupI1 (Proxy @Sym_Foldable) sequenceA_ sequence_ = dupI1 (Proxy @Sym_Foldable) sequence_ traverse_ = dupI2 (Proxy @Sym_Foldable) traverse_ instance ( Read_TypeNameR Text cs rs , Inj_Const cs Foldable ) => Read_TypeNameR Text cs (Proxy Foldable ': rs) where read_typenameR _cs "Foldable" k = k (ty @Foldable) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where show_const ConstZ{} = "Foldable" show_const (ConstS c) = show_const c instance Proj_ConC cs (Proxy Foldable) data instance TokenT meta (ts::[*]) (Proxy Foldable) = Token_Term_Foldable_foldMap (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_foldr (EToken meta ts) (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_foldr' (EToken meta ts) (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_foldl (EToken meta ts) (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_elem (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_null (EToken meta ts) | Token_Term_Foldable_length (EToken meta ts) | Token_Term_Foldable_minimum (EToken meta ts) | Token_Term_Foldable_maximum (EToken meta ts) | Token_Term_Foldable_sum (EToken meta ts) | Token_Term_Foldable_product (EToken meta ts) | Token_Term_Foldable_toList (EToken meta ts) | Token_Term_Foldable_all (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_any (EToken meta ts) (EToken meta ts) | Token_Term_Foldable_and (EToken meta ts) | Token_Term_Foldable_or (EToken meta ts) | Token_Term_Foldable_concat (EToken meta ts) deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Foldable)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Foldable)) instance -- CompileI ( Inj_Const (Consts_of_Ifaces is) Foldable , Inj_Const (Consts_of_Ifaces is) Monoid , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) Int , Inj_Const (Consts_of_Ifaces is) Bool , Inj_Const (Consts_of_Ifaces is) Eq , Inj_Const (Consts_of_Ifaces is) Ord , Inj_Const (Consts_of_Ifaces is) Num , Inj_Const (Consts_of_Ifaces is) [] , Proj_Con (Consts_of_Ifaces is) , Compile is ) => CompileI is (Proxy Foldable) where compileI :: forall meta ctx ret ls rs. TokenT meta is (Proxy Foldable) -> CompileT meta ctx ret is ls (Proxy Foldable ': rs) compileI tok ctx k = case tok of Token_Term_Foldable_foldMap tok_a2m tok_ta -> -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m compileO tok_a2m ctx $ \ty_a2m (TermO a2m) -> compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_type2 (ty @(->)) (At (Just tok_a2m) ty_a2m) $ \Refl ty_a2m_a ty_a2m_m -> check_con (At (Just tok_a2m) (ty @Monoid :$ ty_a2m_m)) $ \Con -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_type (At (Just tok_a2m) ty_a2m_a) (At (Just tok_ta) ty_ta_a) $ \Refl -> k ty_a2m_m $ TermO $ \c -> foldMap (a2m c) (ta c) Token_Term_Foldable_foldr tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr Token_Term_Foldable_foldr' tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr' Token_Term_Foldable_foldl tok_b2a2b tok_b tok_ta -> foldl_from tok_b2a2b tok_b tok_ta foldl Token_Term_Foldable_elem tok_a tok_ta -> -- elem :: (Foldable t, Eq a) => a -> t a -> Bool compileO tok_a ctx $ \ty_a (TermO a) -> compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_con (At (Just tok_ta) (ty @Eq :$ ty_ta_a)) $ \Con -> check_type (At (Just tok_a) ty_a) (At (Just tok_ta) ty_ta_a) $ \Refl -> k (ty @Bool) $ TermO $ \c -> a c `elem` ta c Token_Term_Foldable_null tok_ta -> ta2ty_from tok_ta null Token_Term_Foldable_length tok_ta -> ta2ty_from tok_ta length Token_Term_Foldable_minimum tok_ta -> ta2a_from tok_ta (ty @Ord) minimum Token_Term_Foldable_maximum tok_ta -> ta2a_from tok_ta (ty @Ord) maximum Token_Term_Foldable_sum tok_ta -> ta2a_from tok_ta (ty @Num) sum Token_Term_Foldable_product tok_ta -> ta2a_from tok_ta (ty @Num) product Token_Term_Foldable_toList tok_ta -> -- toList :: Foldable t => t a -> [a] compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> k (ty @[] :$ ty_ta_a) $ TermO $ \c -> toList (ta c) Token_Term_Foldable_all tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta all Token_Term_Foldable_any tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta any Token_Term_Foldable_and tok_tBool -> andor_from tok_tBool and Token_Term_Foldable_or tok_tBool -> andor_from tok_tBool or Token_Term_Foldable_concat tok_tla -> -- concat :: Foldable t => t [a] -> [a] compileO tok_tla ctx $ \ty_tla (TermO tla) -> check_con1 (ty @Foldable) (At (Just tok_tla) ty_tla) $ \Refl Con _ty_tla_t ty_tla_la -> check_type1 (ty @[]) (At (Just tok_tla) ty_tla_la) $ \Refl ty_tla_la_a -> k (ty @[] :$ ty_tla_la_a) $ TermO $ \c -> concat (tla c) where foldr_from tok_a2b2b tok_b tok_ta (fold::forall term f a b. (Sym_Foldable term, Foldable f) => term (a -> b -> b) -> term b -> term (f a) -> term b) = -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b -- foldr' :: Foldable t => (a -> b -> b) -> b -> t a -> b compileO tok_a2b2b ctx $ \ty_a2b2b (TermO a2b2b) -> compileO tok_b ctx $ \ty_b (TermO b) -> compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b) $ \Refl ty_a2b2b_a ty_a2b2b_b2b -> check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b_b2b) $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 -> check_type (At (Just tok_a2b2b) ty_a2b2b_b2b_b0) (At (Just tok_a2b2b) ty_a2b2b_b2b_b1) $ \Refl -> check_type (At (Just tok_a2b2b) ty_a2b2b_b2b_b0) (At (Just tok_b) ty_b) $ \Refl -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_type (At (Just tok_a2b2b) ty_a2b2b_a) (At (Just tok_ta) ty_ta_a) $ \Refl -> k ty_b $ TermO $ \c -> fold (a2b2b c) (b c) (ta c) foldl_from tok_b2a2b tok_b tok_ta (fold::forall term f a b. (Sym_Foldable term, Foldable f) => term (b -> a -> b) -> term b -> term (f a) -> term b) = -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b compileO tok_b2a2b ctx $ \ty_b2a2b (TermO b2a2b) -> compileO tok_b ctx $ \ty_b (TermO b) -> compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b) $ \Refl ty_b2a2b_b ty_b2a2b_a2b -> check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b_a2b) $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b -> check_type (At (Just tok_b2a2b) ty_b2a2b_b) (At (Just tok_b2a2b) ty_b2a2b_a2b_b) $ \Refl -> check_type (At (Just tok_b2a2b) ty_b2a2b_b) (At (Just tok_b) ty_b) $ \Refl -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_type (At (Just tok_b2a2b) ty_b2a2b_a2b_a) (At (Just tok_ta) ty_ta_a) $ \Refl -> k ty_b $ TermO $ \c -> fold (b2a2b c) (b c) (ta c) ta2ty_from :: forall typ. Inj_Const (Consts_of_Ifaces is) typ => EToken meta is -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ) -> Either (Error_Term meta is) ret ta2ty_from tok_ta f = -- length :: Foldable t => t a -> Int -- null :: Foldable t => t a -> Bool compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t _ty_ta_a -> k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $ \c -> f (ta c) ta2a_from :: forall con. EToken meta is -> Type (Consts_of_Ifaces is) con -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a) -> Either (Error_Term meta is) ret ta2a_from tok_ta q f = -- minimum :: (Foldable t, Ord a) => t a -> a -- maximum :: (Foldable t, Ord a) => t a -> a -- sum :: (Foldable t, Num a) => t a -> a -- product :: (Foldable t, Num a) => t a -> a compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_con (At (Just tok_ta) (q :$ ty_ta_a)) $ \Con -> k ty_ta_a $ TermO $ \c -> f (ta c) allany_from tok_a2Bool tok_ta (g::forall term f a. (Sym_Foldable term, Foldable f) => term (a -> Bool) -> term (f a) -> term Bool) = -- all :: Foldable t => (a -> Bool) -> t a -> Bool -- any :: Foldable t => (a -> Bool) -> t a -> Bool compileO tok_a2Bool ctx $ \ty_a2Bool (TermO a2Bool) -> compileO tok_ta ctx $ \ty_ta (TermO ta) -> check_type2 (ty @(->)) (At (Just tok_a2Bool) ty_a2Bool) $ \Refl ty_a2Bool_a ty_a2Bool_Bool -> check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a -> check_type (At (Just tok_a2Bool) ty_a2Bool_a) (At (Just tok_ta) ty_ta_a) $ \Refl -> check_type (At Nothing (ty @Bool)) (At (Just tok_a2Bool) ty_a2Bool_Bool) $ \Refl -> k (ty @Bool) $ TermO $ \c -> g (a2Bool c) (ta c) andor_from tok_tBool (g::forall term f. (Sym_Foldable term, Foldable f) => term (f Bool) -> term Bool) = -- and :: Foldable t => t Bool -> Bool -- or :: Foldable t => t Bool -> Bool compileO tok_tBool ctx $ \ty_tBool (TermO tBool) -> check_con1 (ty @Foldable) (At (Just tok_tBool) ty_tBool) $ \Refl Con _ty_tBool_t ty_tBool_Bool -> check_type (At Nothing (ty @Bool)) (At (Just tok_tBool) ty_tBool_Bool) $ \Refl -> k (ty @Bool) $ TermO $ \c -> g (tBool c)