Language/Symantic/Expr/Foldable.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Foldable'.
  13 module Language.Symantic.Expr.Foldable where
  14
  15 import Control.Monad
  16 import Data.Monoid
  17 import Data.Foldable (Foldable)
  18 import qualified Data.Foldable as Foldable
  19 import Data.Proxy (Proxy(..))
  20 import Data.Type.Equality ((:~:)(Refl))
  21 import Prelude hiding ((<$>), Foldable(..))
  22
  23 import Language.Symantic.Type
  24 import Language.Symantic.Repr
  25 import Language.Symantic.Expr.Root
  26 import Language.Symantic.Expr.Error
  27 import Language.Symantic.Expr.From
  28 import Language.Symantic.Expr.Lambda
  29 import Language.Symantic.Trans.Common
  30
  31 -- * Class 'Sym_Foldable'
  32 -- | Symantic.
  33 class Sym_Foldable repr where
  34         foldMap :: (Foldable f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
  35         foldr   :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  36         foldr'  :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  37         foldl   :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  38         foldl'  :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  39         length  :: Foldable f => repr (f a) -> repr Int
  40         null    :: Foldable f => repr (f a) -> repr Bool
  41         minimum :: (Foldable f, Ord a) => repr (f a) -> repr a
  42         maximum :: (Foldable f, Ord a) => repr (f a) -> repr a
  43         elem    :: (Foldable f, Eq  a) => repr a -> repr (f a) -> repr Bool
  44         sum     :: (Foldable f, Num a) => repr (f a) -> repr a
  45         product :: (Foldable f, Num a) => repr (f a) -> repr a
  46         toList  :: Foldable f => repr (f a) -> repr [a]
  47         default foldMap :: (Trans t repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
  48         default foldr   :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
  49         default foldr'  :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
  50         default foldl   :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
  51         default foldl'  :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
  52         default length  :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
  53         default null    :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
  54         default minimum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  55         default maximum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  56         default elem    :: (Trans t repr, Foldable f, Eq  a) => t repr a -> t repr (f a) -> t repr Bool
  57         default sum     :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  58         default product :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  59         default toList  :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
  60         foldMap = trans_map2 foldMap
  61         foldr   = trans_map3 foldr
  62         foldr'  = trans_map3 foldr'
  63         foldl   = trans_map3 foldl
  64         foldl'  = trans_map3 foldl'
  65         length  = trans_map1 length
  66         null    = trans_map1 null
  67         minimum = trans_map1 minimum
  68         maximum = trans_map1 maximum
  69         elem    = trans_map2 elem
  70         sum     = trans_map1 sum
  71         product = trans_map1 product
  72         toList  = trans_map1 toList
  73 instance Sym_Foldable Repr_Host where
  74         foldMap = liftM2 Foldable.foldMap
  75         foldr   = liftM3 Foldable.foldr
  76         foldr'  = liftM3 Foldable.foldr'
  77         foldl   = liftM3 Foldable.foldl
  78         foldl'  = liftM3 Foldable.foldl'
  79         null    = liftM  Foldable.null
  80         length  = liftM  Foldable.length
  81         minimum = liftM  Foldable.minimum
  82         maximum = liftM  Foldable.maximum
  83         elem    = liftM2 Foldable.elem
  84         sum     = liftM  Foldable.sum
  85         product = liftM  Foldable.product
  86         toList  = liftM  Foldable.toList
  87 instance Sym_Foldable Repr_Text where
  88         foldMap = repr_text_app2 "foldMap"
  89         foldr   = repr_text_app3 "foldr"
  90         foldr'  = repr_text_app3 "foldr'"
  91         foldl   = repr_text_app3 "foldl"
  92         foldl'  = repr_text_app3 "foldl'"
  93         null    = repr_text_app1 "null"
  94         length  = repr_text_app1 "length"
  95         minimum = repr_text_app1 "minimum"
  96         maximum = repr_text_app1 "maximum"
  97         elem    = repr_text_app2 "elem"
  98         sum     = repr_text_app1 "sum"
  99         product = repr_text_app1 "product"
 100         toList  = repr_text_app1 "toList"
 101 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
 102         foldMap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
 103                 foldMap f1 m1 `Repr_Dup` foldMap f2 m2
 104         foldr (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
 105                 foldr f1 a1 m1 `Repr_Dup` foldr f2 a2 m2
 106         foldr' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
 107                 foldr' f1 a1 m1 `Repr_Dup` foldr' f2 a2 m2
 108         foldl (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
 109                 foldl f1 a1 m1 `Repr_Dup` foldl f2 a2 m2
 110         foldl' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
 111                 foldl' f1 a1 m1 `Repr_Dup` foldl' f2 a2 m2
 112         length  (f1 `Repr_Dup` f2) = length  f1 `Repr_Dup` length  f2
 113         null    (f1 `Repr_Dup` f2) = null    f1 `Repr_Dup` null    f2
 114         minimum (f1 `Repr_Dup` f2) = minimum f1 `Repr_Dup` minimum f2
 115         maximum (f1 `Repr_Dup` f2) = maximum f1 `Repr_Dup` maximum f2
 116         elem    (a1 `Repr_Dup` a2) (f1 `Repr_Dup` f2) = elem a1 f1 `Repr_Dup` elem a2 f2
 117         sum     (f1 `Repr_Dup` f2) = sum f1 `Repr_Dup` sum f2
 118         product (f1 `Repr_Dup` f2) = product f1 `Repr_Dup` product f2
 119         toList  (f1 `Repr_Dup` f2) = toList f1 `Repr_Dup` toList f2
 120
 121 -- * Type 'Expr_Foldable'
 122 -- | Expression.
 123 data Expr_Foldable (root:: *)
 124 type instance Root_of_Expr      (Expr_Foldable root)      = root
 125 type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
 126 type instance Sym_of_Expr       (Expr_Foldable root) repr = (Sym_Foldable repr)
 127 type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr
 128
 129 -- | Parse 'foldMap'.
 130 foldMap_from
 131  :: forall root ty ast hs ret.
 132  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 133  , Expr_From ast root
 134  , Type0_Eq ty
 135  , Type0_Lift   Type_Fun (Type_of_Expr root)
 136  , Type0_Unlift Type_Fun (Type_of_Expr root)
 137  , Type0_Constraint Monoid   ty
 138  , Type1_Constraint Foldable ty
 139  , Type1_Unlift (Type_of_Expr root)
 140  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 141                    (Error_of_Expr ast root)
 142  , Root_of_Expr root ~ root
 143  ) => ast -> ast
 144  -> ExprFrom ast (Expr_Foldable root) hs ret
 145 foldMap_from ast_f ast_ta ex ast ctx k =
 146  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 147         expr_from (Proxy::Proxy root) ast_f ctx $
 148          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 149         expr_from (Proxy::Proxy root) ast_ta ctx $
 150          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 151         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_m) ->
 152         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 153         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 154         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 155         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 156         k ty_f_m $ Forall_Repr_with_Context $
 157          \c -> foldMap (f c) (ta c)
 158
 159 -- | Parse 'foldr' or |foldr'|.
 160 foldr_from
 161  :: forall root ty ast hs ret.
 162  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 163  , Expr_From ast root
 164  , Type0_Eq ty
 165  , Type0_Lift   Type_Fun (Type_of_Expr root)
 166  , Type0_Unlift Type_Fun (Type_of_Expr root)
 167  , Type1_Constraint Foldable ty
 168  , Type1_Unlift (Type_of_Expr root)
 169  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 170                    (Error_of_Expr ast root)
 171  , Root_of_Expr root ~ root
 172  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
 173  -> ast -> ast -> ast
 174  -> ExprFrom ast (Expr_Foldable root) hs ret
 175 foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
 176  -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
 177         expr_from (Proxy::Proxy root) ast_f ctx $
 178          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 179         expr_from (Proxy::Proxy root) ast_b ctx $
 180          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 181         expr_from (Proxy::Proxy root) ast_ta ctx $
 182          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 183         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
 184         check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
 185         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 186         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 187         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 188         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 189         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 190         k ty_b $ Forall_Repr_with_Context $
 191          \c -> fold (f c) (b c) (ta c)
 192
 193 -- | Parse 'foldl' or |foldl'|.
 194 foldl_from
 195  :: forall root ty ast hs ret.
 196  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 197  , Expr_From ast root
 198  , Type0_Eq ty
 199  , Type0_Lift   Type_Fun (Type_of_Expr root)
 200  , Type0_Unlift Type_Fun (Type_of_Expr root)
 201  , Type1_Constraint Foldable ty
 202  , Type1_Unlift (Type_of_Expr root)
 203  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 204                    (Error_of_Expr ast root)
 205  , Root_of_Expr root ~ root
 206  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
 207  -> ast -> ast -> ast
 208  -> ExprFrom ast (Expr_Foldable root) hs ret
 209 foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
 210  -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
 211         expr_from (Proxy::Proxy root) ast_f ctx $
 212          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 213         expr_from (Proxy::Proxy root) ast_b ctx $
 214          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 215         expr_from (Proxy::Proxy root) ast_ta ctx $
 216          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 217         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
 218         check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
 219         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 220         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 221         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 222         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 223         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 224         k ty_b $ Forall_Repr_with_Context $
 225          \c -> fold (f c) (b c) (ta c)
 226
 227 -- | Parse 'length'.
 228 length_from
 229  :: forall root ty ast hs ret.
 230  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 231  , Expr_From ast root
 232  , Type0_Eq ty
 233  , Type0_Lift Type_Int (Type_of_Expr root)
 234  , Type1_Constraint Foldable ty
 235  , Type1_Unlift (Type_of_Expr root)
 236  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 237                    (Error_of_Expr ast root)
 238  , Root_of_Expr root ~ root
 239  ) => ast
 240  -> ExprFrom ast (Expr_Foldable root) hs ret
 241 length_from ast_ta ex ast ctx k =
 242  -- length :: Foldable t => t a -> Int
 243         expr_from (Proxy::Proxy root) ast_ta ctx $
 244          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 245         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 246         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 247         k type_int $ Forall_Repr_with_Context $
 248          \c -> length (ta c)
 249
 250 -- | Parse 'null'.
 251 null_from
 252  :: forall root ty ast hs ret.
 253  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 254  , Expr_From ast root
 255  , Type0_Eq ty
 256  , Type0_Lift Type_Bool (Type_of_Expr root)
 257  , Type1_Constraint Foldable ty
 258  , Type1_Unlift (Type_of_Expr root)
 259  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 260                    (Error_of_Expr ast root)
 261  , Root_of_Expr root ~ root
 262  ) => ast
 263  -> ExprFrom ast (Expr_Foldable root) hs ret
 264 null_from ast_ta ex ast ctx k =
 265  -- null :: Foldable t => t a -> Bool
 266         expr_from (Proxy::Proxy root) ast_ta ctx $
 267          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 268         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 269         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 270         k type_bool $ Forall_Repr_with_Context $
 271          \c -> null (ta c)
 272
 273 -- | Parse 'minimum'.
 274 minimum_from
 275  :: forall root ty ast hs ret.
 276  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 277  , Expr_From ast root
 278  , Type0_Eq ty
 279  , Type0_Constraint Ord      ty
 280  , Type1_Constraint Foldable ty
 281  , Type1_Unlift (Type_of_Expr root)
 282  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 283                    (Error_of_Expr ast root)
 284  , Root_of_Expr root ~ root
 285  ) => ast
 286  -> ExprFrom ast (Expr_Foldable root) hs ret
 287 minimum_from ast_ta ex ast ctx k =
 288  -- minimum :: (Foldable t, Ord a) => t a -> a
 289         expr_from (Proxy::Proxy root) ast_ta ctx $
 290          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 291         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 292         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 293         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 294         k ty_t_a $ Forall_Repr_with_Context $
 295          \c -> minimum (ta c)
 296
 297 -- | Parse 'maximum'.
 298 maximum_from
 299  :: forall root ty ast hs ret.
 300  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 301  , Expr_From ast root
 302  , Type0_Eq ty
 303  , Type0_Constraint Ord      ty
 304  , Type1_Constraint Foldable ty
 305  , Type1_Unlift (Type_of_Expr root)
 306  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 307                    (Error_of_Expr ast root)
 308  , Root_of_Expr root ~ root
 309  ) => ast
 310  -> ExprFrom ast (Expr_Foldable root) hs ret
 311 maximum_from ast_ta ex ast ctx k =
 312  -- maximum :: (Foldable t, Ord a) => t a -> a
 313         expr_from (Proxy::Proxy root) ast_ta ctx $
 314          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 315         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 316         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 317         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 318         k ty_t_a $ Forall_Repr_with_Context $
 319          \c -> maximum (ta c)
 320
 321 -- | Parse 'elem'.
 322 elem_from
 323  :: forall root ty ast hs ret.
 324  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 325  , Expr_From ast root
 326  , Type0_Eq ty
 327  , Type0_Constraint  Eq       ty
 328  , Type0_Lift Type_Bool (Type_of_Expr root)
 329  , Type1_Constraint Foldable ty
 330  , Type1_Unlift (Type_of_Expr root)
 331  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 332                    (Error_of_Expr ast root)
 333  , Root_of_Expr root ~ root
 334  ) => ast -> ast
 335  -> ExprFrom ast (Expr_Foldable root) hs ret
 336 elem_from ast_a ast_ta ex ast ctx k =
 337  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 338         expr_from (Proxy::Proxy root) ast_a ctx $
 339          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 340         expr_from (Proxy::Proxy root) ast_ta ctx $
 341          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 342         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 343         check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
 344         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 345         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 346         k type_bool $ Forall_Repr_with_Context $
 347          \c -> a c `elem` ta c
 348
 349 -- | Parse 'sum'.
 350 sum_from
 351  :: forall root ty ast hs ret.
 352  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 353  , Expr_From ast root
 354  , Type0_Eq ty
 355  , Type0_Constraint Num      ty
 356  , Type1_Constraint Foldable ty
 357  , Type1_Unlift (Type_of_Expr root)
 358  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 359                    (Error_of_Expr ast root)
 360  , Root_of_Expr root ~ root
 361  ) => ast
 362  -> ExprFrom ast (Expr_Foldable root) hs ret
 363 sum_from ast_ta ex ast ctx k =
 364  -- sum :: (Foldable t, Num a) => t a -> a
 365         expr_from (Proxy::Proxy root) ast_ta ctx $
 366          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 367         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 368         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 369         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 370         k ty_t_a $ Forall_Repr_with_Context $
 371          \c -> sum (ta c)
 372
 373 -- | Parse 'product'.
 374 product_from
 375  :: forall root ty ast hs ret.
 376  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 377  , Expr_From ast root
 378  , Type0_Eq ty
 379  , Type0_Constraint Num      ty
 380  , Type1_Constraint Foldable ty
 381  , Type1_Unlift (Type_of_Expr root)
 382  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 383                    (Error_of_Expr ast root)
 384  , Root_of_Expr root ~ root
 385  ) => ast
 386  -> ExprFrom ast (Expr_Foldable root) hs ret
 387 product_from ast_ta ex ast ctx k =
 388  -- product :: (Foldable t, Num a) => t a -> a
 389         expr_from (Proxy::Proxy root) ast_ta ctx $
 390          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 391         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 392         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 393         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 394         k ty_t_a $ Forall_Repr_with_Context $
 395          \c -> product (ta c)
 396
 397 -- | Parse 'toList'.
 398 toList_from
 399  :: forall root ty ast hs ret.
 400  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 401  , Expr_From ast root
 402  , Type0_Eq ty
 403  , Type0_Lift Type_List (Type_of_Expr root)
 404  , Type0_Constraint Num      ty
 405  , Type1_Constraint Foldable ty
 406  , Type1_Unlift (Type_of_Expr root)
 407  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 408                    (Error_of_Expr ast root)
 409  , Root_of_Expr root ~ root
 410  ) => ast
 411  -> ExprFrom ast (Expr_Foldable root) hs ret
 412 toList_from ast_ta ex ast ctx k =
 413  -- toList :: Foldable t => t a -> [a]
 414         expr_from (Proxy::Proxy root) ast_ta ctx $
 415          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 416         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 417         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 418         k (type_list ty_t_a) $ Forall_Repr_with_Context $
 419          \c -> toList (ta c)