From c11c6aeda359c91f1d0efb38fa44db7237097240 Mon Sep 17 00:00:00 2001
From: Tim Sheard <sheard@pdx.edu>
Date: Sun, 5 Jan 2025 19:26:57 -0800
Subject: [PATCH] Added Constrained.SumList.hs to repo Defined pickAll the
 basis of sums with fixed length. Added getSizedList as a method of the Foldy
 class getSizeList cost is metered at 1000 calls. Typical calls are less than
 10. Gave HasSpec (optional) method 'typeSpecHasError' a better default value

---
 .../Constrained/Conway/Instances/Basic.hs     |   5 +
 .../Constrained/Conway/Instances/Ledger.hs    |  13 +-
 .../constrained-generators.cabal              |   2 +
 .../src/Constrained/Base.hs                   | 304 ++++++++++++-----
 .../src/Constrained/Examples/Fold.hs          | 173 ++++++++++
 .../src/Constrained/GenT.hs                   |   7 +-
 .../src/Constrained/SumList.hs                | 308 ++++++++++++++++++
 .../test/Constrained/Test.hs                  |  66 +++-
 8 files changed, 792 insertions(+), 86 deletions(-)
 create mode 100644 libs/constrained-generators/src/Constrained/Examples/Fold.hs
 create mode 100644 libs/constrained-generators/src/Constrained/SumList.hs

diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs
index 8ff6c3ade20..b1bdc2de4c6 100644
--- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs
+++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs
@@ -51,6 +51,7 @@ import Cardano.Ledger.Plutus.CostModels (CostModels)
 import Cardano.Ledger.Plutus.ExUnits
 import Cardano.Ledger.Shelley.PParams (ProposedPPUpdates (..))
 import Constrained hiding (Value)
+import Constrained.Base (genListWithSize)
 import Constrained.Univ ()
 import Control.Monad.Identity (Identity (..))
 import Control.Monad.Trans.Fail.String
@@ -95,6 +96,10 @@ instance BaseUniverse fn => Foldy fn Coin where
   genList s s' = map fromSimpleRep <$> genList @fn @Word64 (toSimpleRepSpec s) (toSimpleRepSpec s')
   theAddFn = addFn
   theZero = Coin 0
+  genSizedList sz elemSpec foldSpec =
+    map fromSimpleRep
+      <$> genListWithSize @fn @Word64 sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
+  nonNeg = True
 
 -- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split
 -- this up so that `NumLike` has its own addition etc. instead?
diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs
index 84ce67b50e2..f7fe987e9b1 100644
--- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs
+++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs
@@ -128,7 +128,14 @@ import Cardano.Ledger.UTxO
 import Cardano.Ledger.Val (Val)
 import Constrained hiding (Sized, Value)
 import Constrained qualified as C
-import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..), explainSpecOpt)
+import Constrained.Base (
+  Binder (..),
+  HasGenHint (..),
+  Pred (..),
+  Term (..),
+  explainSpecOpt,
+  genListWithSize,
+ )
 import Constrained.Spec.Map
 import Control.DeepSeq (NFData)
 import Crypto.Hash (Blake2b_224)
@@ -250,6 +257,10 @@ instance IsConwayUniv fn => Foldy fn DeltaCoin where
   genList s s' = map fromSimpleRep <$> genList @fn @Integer (toSimpleRepSpec s) (toSimpleRepSpec s')
   theAddFn = addFn
   theZero = DeltaCoin 0
+  genSizedList sz elemSpec foldSpec =
+    map fromSimpleRep
+      <$> genListWithSize @fn @Integer sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
+  nonNeg = False
 
 deriving via Integer instance Num DeltaCoin
 
diff --git a/libs/constrained-generators/constrained-generators.cabal b/libs/constrained-generators/constrained-generators.cabal
index ce40e7b0d04..0934b42cd07 100644
--- a/libs/constrained-generators/constrained-generators.cabal
+++ b/libs/constrained-generators/constrained-generators.cabal
@@ -26,6 +26,7 @@ library
     Constrained.Examples.Basic
     Constrained.Examples.CheatSheet
     Constrained.Examples.Either
+    Constrained.Examples.Fold
     Constrained.Examples.List
     Constrained.Examples.Map
     Constrained.Examples.Set
@@ -41,6 +42,7 @@ library
     Constrained.Spec.Map
     Constrained.Spec.Pairs
     Constrained.Spec.Tree
+    Constrained.SumList
     Constrained.Syntax
     Constrained.Univ
 
diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
index b064d9ff7d1..9b6fa161d2d 100644
--- a/libs/constrained-generators/src/Constrained/Base.hs
+++ b/libs/constrained-generators/src/Constrained/Base.hs
@@ -87,6 +87,7 @@ import Constrained.GenT
 import Constrained.Graph hiding (dependency, irreflexiveDependencyOn, noDependencies)
 import Constrained.Graph qualified as Graph
 import Constrained.List
+import Constrained.SumList (Cost (..), Solution (..), pickAll)
 import Constrained.Univ
 import Data.List.NonEmpty (NonEmpty ((:|)))
 import Data.List.NonEmpty qualified as NE
@@ -422,9 +423,7 @@ data HOLE a b where
 
 toCtx ::
   forall m fn v a.
-  ( BaseUniverse fn
-  , Typeable v
-  , MonadGenError m
+  ( MonadGenError m
   , HasCallStack
   , HasSpec fn a
   , HasSpec fn v
@@ -457,7 +456,7 @@ toCtx v t
 
 toCtxList ::
   forall m fn v as.
-  (BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v, MonadGenError m, HasCallStack) =>
+  (All (HasSpec fn) as, HasSpec fn v, MonadGenError m, HasCallStack) =>
   Var v ->
   List (Term fn) as ->
   m (ListCtx Value as (Ctx fn v))
@@ -659,7 +658,7 @@ instance HasSpec fn a => Semigroup (Specification fn a) where
   ErrorSpec e <> ErrorSpec e' =
     ErrorSpec
       ( e
-          <> pure ("------ spec <> spec ------ @" ++ show (typeRep (Proxy @a)))
+          <> pure ("------ spec <> spec ------ @" ++ showType @a)
           <> e'
       )
   ErrorSpec e <> _ = ErrorSpec e
@@ -677,7 +676,7 @@ instance HasSpec fn a => Semigroup (Specification fn a) where
     memberSpecList
       (nub $ NE.filter (`conformsToSpec` ts) as)
       ( NE.fromList
-          [ "The two " ++ show (typeRep (Proxy @a)) ++ " Specifications are inconsistent."
+          [ "The two " ++ showType @a ++ " Specifications are inconsistent."
           , "  " ++ show ms
           , "  " ++ show ts
           ]
@@ -903,9 +902,13 @@ class
 
   -- Each instance can decide if a TypeSpec has an Error, and what String
   -- to pass to ErrorSpec to create an ErrorSpec value. Particulary
-  -- useful for type Sum and Prod
+  -- useful for type Sum and Prod. The default instance uses guardTypeSpec,
+  -- which also has a default value, and if that is used, typeSpecHasError will
+  -- return Nothing. Both 'typeSpecHasError' and 'guardTypeSpec' can be set individually.
   typeSpecHasError :: TypeSpec fn a -> Maybe (NE.NonEmpty String)
-  typeSpecHasError _ = Nothing
+  typeSpecHasError tspec = case guardTypeSpec @fn @a [] tspec of
+    ErrorSpec msgs -> Just msgs
+    _ -> Nothing
 
   -- Some binary TypeSpecs, which nest to the right
   -- e.g. something like this (X a (TypeSpec (X b (TypeSpec (X c w))))))
@@ -927,6 +930,9 @@ class
   typeSpecOpt tySpec bad = TypeSpec tySpec bad
 
   -- | This can be used to detect self inconsistencies in a (TypeSpec fn t)
+  --   Note this is similar to 'typeSpecHasError', and the default
+  --   value for 'typeSpecHasError' is written in terms of 'guadTypeSpec'
+  --   Both 'typeSpecHasError' and 'guardTypeSpec' can be set individually.
   guardTypeSpec :: [String] -> TypeSpec fn a -> Specification fn a
   guardTypeSpec _ ty = typeSpec ty
 
@@ -1158,10 +1164,12 @@ genFromSpecT (simplifySpec -> spec) = case spec of
     mode <- getMode
     explain
       ( NE.fromList
-          [ "genFromSpecT at type " ++ show (typeRep cant)
-          , "    " ++ show spec
-          , "  with mode " ++ show mode
-          , "  cant set {" ++ unlines (map show cant) ++ "}"
+          [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a
+          , "tspec = "
+          , show s
+          , "cant = "
+          , unlines (map (\x -> "  " ++ show x) cant)
+          , "with mode " ++ show mode
           ]
       )
       $
@@ -1291,11 +1299,23 @@ genFromSpecWithSeed ::
   forall fn a. (HasCallStack, HasSpec fn a) => Int -> Int -> Specification fn a -> a
 genFromSpecWithSeed seed size spec = unGen (genFromSpec spec) (mkQCGen seed) size
 
+-- | A version of `genFromSpecT` that runs in the IO monad. Good for debugging.
+debugSpec :: forall fn a. HasSpec fn a => Specification fn a -> IO ()
+debugSpec spec = do
+  ans <- generate $ genFromGenT $ inspect (genFromSpecT spec)
+  let f x = putStrLn (unlines (NE.toList x))
+      ok x =
+        if conformsToSpec x spec
+          then putStrLn "True"
+          else putStrLn "False, perhaps there is an unsafeExists in the spec?"
+  case ans of
+    FatalError xs x -> mapM f xs >> f x
+    GenError xs x -> mapM f xs >> f x
+    Result _ x -> print spec >> print x >> ok x
+
 genInverse ::
   ( MonadGenError m
   , HasSpec fn a
-  , Show b
-  , Functions fn fn
   , HasSpec fn b
   ) =>
   fn '[a] b ->
@@ -1583,7 +1603,7 @@ short [x] =
   let raw = show x
       refined = if length raw <= 20 then raw else take 20 raw ++ " ... "
    in "[" <+> fromString refined <+> "]"
-short xs = "([" <+> viaShow (length xs) <+> "elements ...] @" <> viaShow (typeRep (Proxy @a)) <> ")"
+short xs = "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <> ")"
 
 prettyPlan :: HasSpec fn a => Specification fn a -> Doc ann
 prettyPlan (simplifySpec -> spec)
@@ -1650,7 +1670,7 @@ genFromPreds env0 (optimisePred . optimisePred -> preds) =
     plan <- runGE $ prepareLinearization @fn preds
     go env0 plan
   where
-    go :: MonadGenError m => Env -> SolverPlan fn -> GenT m Env
+    go :: Env -> SolverPlan fn -> GenT m Env
     go env plan | isEmptyPlan plan = pure env
     go env plan = do
       (env', plan') <-
@@ -1739,7 +1759,7 @@ normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec'
 -- Computing specs
 ------------------------------------------------------------------------
 
-fromGESpec :: (HasCallStack, HasSpec fn a) => GE (Specification fn a) -> Specification fn a
+fromGESpec :: HasCallStack => GE (Specification fn a) -> Specification fn a
 fromGESpec ge = case ge of
   Result [] s -> s
   Result es s -> addToErrorSpec (foldr1 (<>) es) s
@@ -1834,7 +1854,7 @@ computeSpecSimplified x p = localGESpec $ case p of
   Case (Lit val) bs -> runCaseOn val (mapList thing bs) $ \va vaVal psa -> computeSpec x (substPred (singletonEnv va vaVal) psa)
   Case t branches -> do
     branchSpecs <- mapMList (traverseWeighted computeSpecBinderSimplified) branches
-    propagateSpec (caseSpec (Just (show (typeRep (Proxy @a)))) branchSpecs) <$> toCtx x t
+    propagateSpec (caseSpec (Just (showType @a)) branchSpecs) <$> toCtx x t
   When (Lit b) tp -> if b then computeSpecSimplified x tp else pure TrueSpec
   -- This shouldn't happen a lot of the time because when the body is trivial we mostly get rid of the `When` entirely
   When {} -> pure $ SuspendedSpec x p
@@ -2522,7 +2542,7 @@ optimisePred p =
     $ p
 
 -- Common subexpression elimination but only on terms that are already let-bound.
-letSubexpressionElimination :: BaseUniverse fn => Pred fn -> Pred fn
+letSubexpressionElimination :: Pred fn -> Pred fn
 letSubexpressionElimination = go []
   where
     adjustSub x sub =
@@ -3084,6 +3104,12 @@ class HasSpec fn a => Foldy fn a where
     (BaseUniverse fn, MonadGenError m) => Specification fn a -> Specification fn a -> GenT m [a]
   theAddFn :: fn '[a, a] a
   theZero :: a
+  genSizedList ::
+    (BaseUniverse fn, MonadGenError m) =>
+    Specification fn Integer -> Specification fn a -> Specification fn a -> GenT m [a]
+  nonNeg :: Bool
+
+-- genSizedList = genListWithSize
 
 adds :: forall fn a. Foldy fn a => [a] -> a
 adds = foldr (sem $ theAddFn @fn) (theZero @fn)
@@ -3102,7 +3128,7 @@ data FoldSpec (fn :: [Type] -> Type -> Type) a where
     Specification fn b ->
     FoldSpec fn a
 
-instance {-# OVERLAPPABLE #-} (Arbitrary a, Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) => Arbitrary (FoldSpec fn a) where
+instance {-# OVERLAPPABLE #-} (Arbitrary (TypeSpec fn a), Foldy fn a, BaseUniverse fn) => Arbitrary (FoldSpec fn a) where
   arbitrary = oneof [FoldSpec idFn <$> arbitrary, pure NoFold]
   shrink NoFold = []
   shrink (FoldSpec (extractFn @(FunFn fn) @fn -> Just Id) spec) = FoldSpec idFn <$> shrink spec
@@ -3133,7 +3159,7 @@ toPredsFoldSpec x (FoldSpec fn sspec) =
   satisfies (app (foldMapFn fn) x) sspec
 
 -- | Note: potentially infinite list
-enumerateInterval :: (Enum a, Num a, Ord a, MaybeBounded a) => NumSpec fn a -> [a]
+enumerateInterval :: (Enum a, Num a, MaybeBounded a) => NumSpec fn a -> [a]
 enumerateInterval (NumSpecInterval lo hi) =
   case (lo <|> lowerBound, hi <|> upperBound) of
     (Nothing, Nothing) -> interleave [0 ..] [-1, -2 ..]
@@ -3191,12 +3217,10 @@ knownLowerBound (TypeSpec (NumSpecInterval lo hi) cant) =
 
 narrowByFuelAndSize ::
   forall a fn.
-  ( BaseUniverse fn
-  , TypeSpec fn a ~ NumSpec fn a
+  ( TypeSpec fn a ~ NumSpec fn a
   , HasSpec fn a
   , Arbitrary a
   , Integral a
-  , Ord a
   , Random a
   , MaybeBounded a
   ) =>
@@ -3316,12 +3340,10 @@ narrowByFuelAndSize fuel size specs =
 
 narrowFoldSpecs ::
   forall a fn.
-  ( BaseUniverse fn
-  , TypeSpec fn a ~ NumSpec fn a
+  ( TypeSpec fn a ~ NumSpec fn a
   , HasSpec fn a
   , Arbitrary a
   , Integral a
-  , Ord a
   , Random a
   , MaybeBounded a
   ) =>
@@ -3386,16 +3408,13 @@ narrowFoldSpecs specs = maybe specs narrowFoldSpecs (go specs)
 
 genNumList ::
   forall a fn m.
-  ( BaseUniverse fn
-  , MonadGenError m
+  ( MonadGenError m
   , TypeSpec fn a ~ NumSpec fn a
-  , HasSpec fn a
   , Arbitrary a
   , Integral a
-  , Ord a
-  , Random a
   , MaybeBounded a
   , Foldy fn a
+  , Random a
   ) =>
   Specification fn a ->
   Specification fn a ->
@@ -3496,56 +3515,78 @@ instance BaseUniverse fn => Foldy fn Int where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Integer where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Int8 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Int16 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Int32 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Int64 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = False
 
 instance BaseUniverse fn => Foldy fn Word8 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = True
 
 instance BaseUniverse fn => Foldy fn Word16 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = True
 
 instance BaseUniverse fn => Foldy fn Word32 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = True
 
 instance BaseUniverse fn => Foldy fn Word64 where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = True
 
 instance BaseUniverse fn => Foldy fn Natural where
   genList = genNumList
   theAddFn = injectFn (Add @fn)
   theZero = 0
+  genSizedList = genListWithSize
+  nonNeg = True
 
 genFromFold ::
   forall m fn a b.
@@ -3559,7 +3600,16 @@ genFromFold ::
   fn '[a] b ->
   Specification fn b ->
   GenT m [a]
-genFromFold (nub -> must) (simplifySpec -> size) elemS fn foldS =
+genFromFold _ (simplifySpec -> size) _ _ _
+  | isErrorLike size =
+      fatalError (NE.cons "genFromFold has ErrorLike sizeSpec" (errorLikeMessage size))
+genFromFold _ _ elemS _ _
+  | isErrorLike elemS =
+      fatalError (NE.cons "genFromFold has ErrorLike elemSpec" (errorLikeMessage elemS))
+genFromFold _ _ _ _ foldS
+  | isErrorLike foldS =
+      fatalError (NE.cons "genFromFold has ErrorLike totalSpec" (errorLikeMessage foldS))
+genFromFold must (simplifySpec -> size) elemS fn foldS =
   explain
     ( NE.fromList
         [ "while calling genFromFold"
@@ -3575,18 +3625,8 @@ genFromFold (nub -> must) (simplifySpec -> size) elemS fn foldS =
           mustVal = adds @fn (map (sem fn) must)
           foldS' = propagateSpecFun (theAddFn @fn) (HOLE :? Value mustVal :> Nil) foldS
           sizeSpec' = propagateSpecFun (addFn @fn) (HOLE :? Value (sizeOf must) :> Nil) size
-      m <- getMode
       when (isErrorLike sizeSpec') $ genError1 "Inconsistent size spec"
-      results0 <-
-        withMode Loose $
-          ( withMode m $
-              -- TODO: this is not the best solution to this problem, we need
-              -- to use the size information in `genList` instead
-              suchThatWithTryT
-                10
-                (genList (simplifySpec elemS') (simplifySpec foldS'))
-                (\xs -> sizeOf xs `conformsToSpec` sizeSpec')
-          )
+      results0 <- genSizedList sizeSpec' (simplifySpec elemS') (simplifySpec foldS')
       results <-
         explain
           ( NE.fromList
@@ -4157,7 +4197,7 @@ instance HasSpec fn a => Pretty (WithPrec (FoldSpec fn a)) where
     parensIf (d > 10) $
       "FoldSpec"
         /> vsep'
-          [ "fn   =" <+> viaShow fn
+          [ "fn   =" <+> parens (hsep ["injectFn", "$", viaShow fn])
           , "spec =" <+> pretty s
           ]
 
@@ -4214,7 +4254,7 @@ instance HasSpec fn a => HasSpec fn [a] where
 
   genFromTypeSpec (ListSpec _ must _ elemS _)
     | any (not . (`conformsToSpec` elemS)) must =
-        genError1 "genTypeSpecSpec @ListSpec: must do not conform to elemS"
+        genError1 "genTypeSpecSpec @ListSpec: some elements of mustSet do not conform to elemS"
   genFromTypeSpec (ListSpec msz must TrueSpec elemS NoFold) = do
     lst <- case msz of
       Nothing -> listOfT $ genFromSpecT elemS
@@ -4231,8 +4271,9 @@ instance HasSpec fn a => HasSpec fn [a] where
         sz
         ((`conformsToSpec` szSpec) . (+ sizeOf must) . fromIntegral)
     pureGen $ shuffle (must ++ lst)
-  genFromTypeSpec (ListSpec msz must size elemS (FoldSpec f foldS)) = do
-    genFromFold must (size <> maybe TrueSpec leqSpec msz) elemS f foldS
+  genFromTypeSpec (ListSpec msz must szSpec elemS (FoldSpec f foldS)) = do
+    let szSpec' = (szSpec <> maybe TrueSpec (leqSpec . max 0) msz)
+    genFromFold must szSpec' elemS f foldS
 
   shrinkWithTypeSpec (ListSpec _ _ _ es _) as =
     shrinkList (shrinkWithSpec es) as
@@ -4609,8 +4650,7 @@ idFn :: forall fn a. Member (FunFn fn) fn => fn '[a] a
 idFn = injectFn $ Id @fn
 
 composeFn ::
-  ( Member (FunFn fn) fn
-  , HasSpec fn b
+  ( HasSpec fn b
   , Show (fn '[a] b)
   , Show (fn '[b] c)
   , Eq (fn '[a] b)
@@ -4623,10 +4663,7 @@ composeFn f g = injectFn $ Compose f g
 
 flip_ ::
   forall fn a b c.
-  ( Member (FunFn fn) fn
-  , Typeable a
-  , Typeable b
-  , HasSpec fn a
+  ( HasSpec fn a
   , HasSpec fn b
   , HasSpec fn c
   ) =>
@@ -4688,7 +4725,7 @@ instance FunctionLike fn => FunctionLike (FunFn fn) where
     Compose f g -> sem f . sem g
     Flip f -> flip (sem f)
 
-instance (BaseUniverse fn, Member (FunFn fn) fn) => Functions (FunFn fn) fn where
+instance BaseUniverse fn => Functions (FunFn fn) fn where
   propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err
   propagateSpecFun fn ctx spec = case fn of
     Id | NilCtx HOLE <- ctx -> spec
@@ -4957,7 +4994,7 @@ foldMapFn f = injectFn $ FoldMap @fn f
 singletonListFn :: forall fn a. HasSpec fn a => fn '[a] [a]
 singletonListFn = injectFn $ SingletonList @fn
 
-appendFn :: forall fn a. (HasSpec fn a, Show a, Typeable a) => fn '[[a], [a]] [a]
+appendFn :: forall fn a. HasSpec fn a => fn '[[a], [a]] [a]
 appendFn = injectFn $ AppendFn @a @fn
 
 -- Number functions -------------------------------------------------------
@@ -5024,7 +5061,7 @@ instance {-# OVERLAPPABLE #-} (HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSp
     , Nothing <- safeSubtract @fn a u =
         ErrorSpec $
           NE.fromList
-            [ "Underflow in subtractSpec (" ++ show (typeOf a) ++ "):"
+            [ "Underflow in subtractSpec (" ++ showType @a ++ "):"
             , "  a = " ++ show a
             , "  ts = " ++ show ts
             ]
@@ -5033,7 +5070,7 @@ instance {-# OVERLAPPABLE #-} (HasSpec fn a, Ord a, Num a, TypeSpec fn a ~ NumSp
     , Nothing <- safeSubtract @fn a l =
         ErrorSpec $
           NE.fromList
-            [ "Overflow in subtractSpec (" ++ show (typeOf a) ++ "):"
+            [ "Overflow in subtractSpec (" ++ showType @a ++ "):"
             , "  a = " ++ show a
             , "  ts = " ++ show ts
             ]
@@ -5273,18 +5310,14 @@ infix 4 <=., >=., >., <., ==., /=.
 a /=. b = not_ (a ==. b)
 
 sum_ ::
-  ( BaseUniverse fn
-  , Member (FunFn fn) fn
-  , Foldy fn a
-  ) =>
+  Foldy fn a =>
   Term fn [a] ->
   Term fn a
 sum_ = foldMap_ id
 
 foldMap_ ::
   forall fn a b.
-  ( BaseUniverse fn
-  , Foldy fn b
+  ( Foldy fn b
   , HasSpec fn a
   ) =>
   (Term fn a -> Term fn b) ->
@@ -5603,6 +5636,12 @@ instance HasSpec fn a => Pretty (WithPrec (Term fn a)) where
           prettyPrec p a
       | otherwise -> parensIf (p > 10) $ viaShow f <+> align (fillSep (ppList @fn (prettyPrec 11) as))
 
+showType :: forall t. Typeable t => String
+showType = show (typeRep (Proxy @t))
+
+prettyType :: forall t x. Typeable t => Doc x
+prettyType = fromString $ show (typeRep (Proxy @t))
+
 instance HasSpec fn a => Pretty (Term fn a) where
   pretty = prettyPrec 0
 
@@ -5630,7 +5669,7 @@ instance Pretty (Pred fn) where
     TruePred -> "True"
     FalsePred {} -> "False"
     Monitor {} -> "monitor"
-    Explain es p -> "ExplainPred" <+> viaShow (NE.toList es) <+> "$" /> pretty p
+    Explain es p -> "Explain" <+> viaShow (NE.toList es) <+> "$" /> pretty p
 
 -- TODO: make nicer
 instance Pretty (f a) => Pretty (Weighted f a) where
@@ -5650,8 +5689,10 @@ instance HasSpec fn a => Pretty (WithPrec (Specification fn a)) where
   pretty (WithPrec d s) = case s of
     ExplainSpec es s -> "ExplainSpec" <+> viaShow es <+> "$" /> pretty s
     ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es))
-    TrueSpec -> fromString $ "TrueSpec @(" ++ show (typeRep (Proxy @a)) ++ ")"
-    MemberSpec xs -> "MemberSpec" <+> short (NE.toList xs)
+    TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")"
+    MemberSpec xs ->
+      "MemberSpec"
+        <+> short (NE.toList xs)
     SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p
     -- TODO: require pretty for `TypeSpec` to make this much nicer
     TypeSpec ts cant ->
@@ -5694,7 +5735,7 @@ deriving instance Show (SizeFn fn as b)
 instance FunctionLike (SizeFn fn) where
   sem SizeOf = sizeOf @fn -- From the Sized class
 
-sizeOfFn :: forall fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized fn a) => fn '[a] Integer
+sizeOfFn :: forall fn a. (HasSpec fn a, Sized fn a) => fn '[a] Integer
 sizeOfFn = injectFn $ SizeOf @fn @a
 
 -- Operations on Size (specified in SizeFn) by the Functions instance
@@ -5727,6 +5768,9 @@ rangeSize :: Integer -> Integer -> SizeSpec fn
 rangeSize a b | a < 0 || b < 0 = error ("Negative Int in call to rangeSize: " ++ show a ++ " " ++ show b)
 rangeSize a b = NumSpecInterval (Just a) (Just b)
 
+between :: (HasSpec fn a, TypeSpec fn a ~ NumSpec fn a) => a -> a -> Specification fn a
+between lo hi = TypeSpec (NumSpecInterval (Just lo) (Just hi)) []
+
 -- | The widest interval whose largest element is admitted by the original spec
 maxSpec :: BaseUniverse fn => Specification fn Integer -> Specification fn Integer
 maxSpec (ExplainSpec es s) = explainSpecOpt es (maxSpec s)
@@ -5770,9 +5814,7 @@ class Sized fn t where
 
   sizeOfTypeSpec :: HasSpec fn t => TypeSpec fn t -> Specification fn Integer
   default sizeOfTypeSpec ::
-    ( HasSpec fn t
-    , HasSpec fn (SimpleRep t)
-    , HasSimpleRep t
+    ( HasSpec fn (SimpleRep t)
     , Sized fn (SimpleRep t)
     , TypeSpec fn t ~ TypeSpec fn (SimpleRep t)
     ) =>
@@ -5805,7 +5847,7 @@ hasSize sz = liftSizeSpec sz []
 -- Given operator ☉, then (a,b) ☉ (c,d) = (minimum s, maximum s) where s = [a ☉ c, a ☉ d, b ☉ c, b ☉ d]
 -- There are simpler rules for (+) and (-), but for (*) we need to use the general rule.
 
-guardEmpty :: Maybe Integer -> Maybe Integer -> NumSpec fn Integer -> NumSpec fn Integer
+guardEmpty :: (Ord n, Num n) => Maybe n -> Maybe n -> NumSpec fn n -> NumSpec fn n
 guardEmpty (Just a) (Just b) s
   | a <= b = s
   | otherwise = NumSpecInterval (Just 1) (Just 0)
@@ -5823,7 +5865,7 @@ subNumSpec (NumSpecInterval x y) (NumSpecInterval a b) =
     guardEmpty a b $
       NumSpecInterval ((-) <$> x <*> b) ((-) <$> y <*> a)
 
-multNumSpec :: NumSpec fn Integer -> NumSpec fn Integer -> NumSpec fn Integer
+multNumSpec :: (Ord n, Num n) => NumSpec fn n -> NumSpec fn n -> NumSpec fn n
 multNumSpec (NumSpecInterval a b) (NumSpecInterval c d) =
   guardEmpty a b $
     guardEmpty c d $
@@ -5918,7 +5960,7 @@ operateSpec operator f ft x y = case (x, y) of
 --   Here we lift the HasSpec methods 'cardinalTrueSpec' and 'cardinalTypeSpec'
 --   from (TypeSpec fn Integer) to (Specification fn Integer)
 cardinality ::
-  forall fn a. (Eq a, BaseUniverse fn, HasSpec fn a) => Specification fn a -> Specification fn Integer
+  forall fn a. HasSpec fn a => Specification fn a -> Specification fn Integer
 cardinality (ExplainSpec es s) = explainSpecOpt es (cardinality s)
 cardinality TrueSpec = cardinalTrueSpec @fn @a
 cardinality (MemberSpec es) = equalSpec (sizeOf (nub (NE.toList es)))
@@ -5933,7 +5975,7 @@ cardinality SuspendedSpec {} = cardinalTrueSpec @fn @a
 --   cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn Integer
 --   for types 'n' such that (TypeSpec n ~ NumSpec n)
 cardinalNumSpec ::
-  forall n fn. (Integral n, Num n, MaybeBounded n) => NumSpec fn n -> Specification fn Integer
+  forall n fn. (Integral n, MaybeBounded n) => NumSpec fn n -> Specification fn Integer
 cardinalNumSpec (NumSpecInterval (Just lo) (Just hi)) =
   if hi >= lo then MemberSpec (pure (toInteger hi - toInteger lo + 1)) else MemberSpec (pure 0)
 cardinalNumSpec (NumSpecInterval Nothing (Just hi)) =
@@ -5983,9 +6025,7 @@ finiteSize = toInteger (maxBound @n) - toInteger (minBound @n) + 1
 --      the count of interval is. We only need the (length badlist > (N/2)).
 notInNumSpec ::
   forall fn n.
-  ( Functions fn fn
-  , BaseUniverse fn
-  , HasSpec fn n
+  ( HasSpec fn n
   , TypeSpec fn n ~ NumSpec fn n
   , Bounded n
   , Integral n
@@ -6062,7 +6102,7 @@ multT PosInf (Ok _) = PosInf
 --   Because many (TypeSpec fn t)'s contain (Specification fn s), for types 's' different from 't'
 sizeOfSpec ::
   forall fn t.
-  (BaseUniverse fn, Sized fn t, HasSpec fn t) => Specification fn t -> Specification fn Integer
+  (Sized fn t, HasSpec fn t) => Specification fn t -> Specification fn Integer
 sizeOfSpec (ExplainSpec _ s) = sizeOfSpec s
 sizeOfSpec TrueSpec = TrueSpec
 sizeOfSpec s@(MemberSpec xs) = nubOrdMemberSpec ("call to (sizeOfSpec " ++ show s ++ ")") (map (sizeOf @fn) (NE.toList xs))
@@ -6240,3 +6280,109 @@ conformsToSpecE a (SuspendedSpec v ps) msgs =
     Nothing -> Nothing
     Just es -> Just (pure ("conformsToSpecE SuspendedSpec case on var " ++ show v ++ " fails") <> es)
 conformsToSpecE _ (ErrorSpec es) msgs = Just (msgs <> pure "conformsToSpecE ErrorSpec case" <> es)
+
+-- =====================================================================================
+
+-- | Generate a list with 'sizeSpec' elements, that add up to a total that conforms
+--   to 'foldSpec'. Every element in the list should conform to 'elemSpec'
+genListWithSize ::
+  forall fn a m.
+  (Foldy fn a, MonadGenError m, Random a, Integral a, TypeSpec fn a ~ NumSpec fn a) =>
+  Specification fn Integer -> Specification fn a -> Specification fn a -> GenT m [a]
+genListWithSize sizespec elemSpec foldSpec
+  | ErrorSpec _ <- sizespec <> geqSpec 0 =
+      fatalError
+        ( NE.fromList
+            [ "genListWithSize called with possible negative size"
+            , "  sizeSpec = " ++ specName sizespec
+            , "  elemSpec = " ++ specName elemSpec
+            , "  foldSpec = " ++ specName foldSpec
+            ]
+        )
+genListWithSize TrueSpec elemSpec foldSpec = genList elemSpec foldSpec
+genListWithSize sizespec elemSpec foldSpec =
+  let message =
+        [ "\nGenSizedList fails"
+        , "sizespec = " ++ specName sizespec
+        , "elemSpec = " ++ specName elemSpec
+        , "foldSpec = " ++ specName foldSpec
+        , "size adjusted = " ++ show (sizespec <> geqSpec 0)
+        ]
+   in push message $
+        do
+          count <- genFromSpecT (sizespec <> geqSpec 0) -- Sizes cannot be negative.
+          total <- genFromSpecT foldSpec
+          case compare total 0 of
+            EQ ->
+              if conformsToSpec 0 sizespec
+                then pure []
+                else
+                  if nonNeg @fn @a
+                    then
+                      fatalError1
+                        ("Can't find a non-zero number of things that add to 0 at type " ++ showType @a)
+                    else pickNegative elemSpec total count
+            GT -> pickPositive @fn elemSpec total count
+            LT -> pickNegative elemSpec total count
+
+pickPositive ::
+  forall fn t m.
+  (Integral t, Random t, MonadGenError m, Foldy fn t, TypeSpec fn t ~ NumSpec fn t) =>
+  Specification fn t -> t -> Integer -> GenT m [t]
+pickPositive elemspec total count = do
+  let smallest =
+        if nonNeg @fn @t
+          then 0
+          else
+            if total < 0
+              then smallestFromSpec (negate (div total 4)) elemspec
+              else smallestFromSpec 0 elemspec
+  sol <- pureGen $ pickAll smallest (predSpecPair elemspec) total (fromInteger count) (Cost 0)
+  case sol of
+    (_, No msgs) -> fatalError (NE.fromList msgs)
+    (_, Yes (x :| _)) -> pure x
+
+pickNegative ::
+  forall fn t m.
+  (Integral t, Random t, MonadGenError m, TypeSpec fn t ~ NumSpec fn t, HasSpec fn t) =>
+  Specification fn t -> t -> Integer -> GenT m [t]
+
+-- | total can be either negative, or 0. If it is 0, we want count numbers that add to zero
+pickNegative elemspec total count = do
+  sol <-
+    pureGen $
+      pickAll
+        (smallestFromSpec (total - 10) elemspec)
+        (predSpecPair elemspec)
+        total
+        (fromInteger count)
+        (Cost 0)
+  case sol of
+    (_, No msgs) -> fatalError (NE.fromList msgs)
+    (_, Yes (x :| _)) -> pure x
+
+specName :: forall fn a. HasSpec fn a => Specification fn a -> String
+specName (ExplainSpec [x] _) = x
+specName x = show x
+
+predSpecPair :: forall fn a. HasSpec fn a => Specification fn a -> (String, a -> Bool)
+predSpecPair spec = (specName spec, (`conformsToSpec` spec))
+
+-- | The smallest number admitted by the spec, if there is one
+minFromSpec ::
+  forall fn n.
+  (Ord n, TypeSpec fn n ~ NumSpec fn n, BaseUniverse fn) =>
+  Specification fn n -> Maybe n
+minFromSpec (ExplainSpec _ spec) = minFromSpec @fn @n spec
+minFromSpec TrueSpec = Nothing
+minFromSpec s@(SuspendedSpec _ _) =
+  case (simplifySpec s) of
+    (SuspendedSpec _ _) -> Nothing
+    x -> minFromSpec @fn @n x
+minFromSpec (ErrorSpec _) = Nothing
+minFromSpec (MemberSpec xs) = Just (minimum xs)
+minFromSpec (TypeSpec (NumSpecInterval lo _) _) = lo
+
+smallestFromSpec ::
+  (TypeSpec fn p ~ NumSpec fn p, Ord p, BaseUniverse fn) => p -> Specification fn p -> p
+smallestFromSpec n spec = maybe n id (minFromSpec spec)
diff --git a/libs/constrained-generators/src/Constrained/Examples/Fold.hs b/libs/constrained-generators/src/Constrained/Examples/Fold.hs
new file mode 100644
index 00000000000..59ddbecb7e2
--- /dev/null
+++ b/libs/constrained-generators/src/Constrained/Examples/Fold.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Constrained.Examples.Fold where
+
+import Constrained
+import Constrained.Base (Pred (..), genListWithSize, predSpecPair)
+import Constrained.Examples.List (Numbery)
+import Constrained.SumList
+import Data.List.NonEmpty (NonEmpty ((:|)))
+import qualified Data.List.NonEmpty as NE
+import Data.String (fromString)
+import Prettyprinter (fillSep, punctuate, space)
+import System.Random (Random)
+import Test.QuickCheck hiding (forAll, total)
+
+-- ========================================================
+-- Specifications we use in the examples and in the tests
+
+oddSpec :: Specification BaseFn Int
+oddSpec = ExplainSpec ["odd via (y+y+1)"] $
+  constrained $ \ [var|oddx|] ->
+    exists
+      (\eval -> pure (div (eval oddx - 1) 2))
+      (\ [var|y|] -> [Assert $ oddx ==. y + y + 1])
+
+evenSpec ::
+  forall n.
+  (TypeSpec BaseFn n ~ NumSpec BaseFn n, Integral n, HasSpec BaseFn n, MaybeBounded n) =>
+  Specification BaseFn n
+evenSpec = ExplainSpec ["even via (x+x)"] $
+  constrained $ \ [var|evenx|] ->
+    exists
+      (\eval -> pure (div (eval evenx) 2))
+      (\ [var|somey|] -> [Assert $ evenx ==. somey + somey])
+
+sum3WithLength :: Integer -> Specification BaseFn ([Int], Int, Int, Int)
+sum3WithLength n =
+  constrained $ \ [var|quad|] ->
+    match quad $ \ [var|l|] [var|n1|] [var|n2|] [var|n3|] ->
+      [ Assert $ sizeOf_ l ==. lit n
+      , forAll l $ \ [var|item|] -> item >=. lit 0
+      , Assert $ sum_ l ==. n1 + n2 + n3
+      , Assert $ n1 + n2 + n3 >=. lit (fromInteger n)
+      ]
+
+sum3 :: Specification BaseFn [Int]
+sum3 = constrained $ \ [var|xs|] -> [sum_ xs ==. lit 6 + lit 9 + lit 5, sizeOf_ xs ==. 5]
+
+listSumPair :: Numbery a => Specification BaseFn [(a, Int)]
+listSumPair = constrained $ \xs ->
+  [ assert $ foldMap_ fst_ xs ==. 100
+  , forAll' xs $ \x y -> [20 <. x, x <. 30, y <. 100]
+  ]
+
+listSumForall :: Numbery a => Specification BaseFn [a]
+listSumForall = constrained $ \xs ->
+  [ forAll xs $ \x -> 1 <. x
+  , assert $ sum_ xs ==. 20
+  ]
+
+-- | Complicated, because if 'a' is too large, the spec is unsatisfiable.
+listSumComplex :: Numbery a => a -> Specification BaseFn [a]
+listSumComplex a = constrained $ \xs ->
+  [ forAll xs $ \x -> 1 <. x
+  , assert $ sum_ xs ==. 20
+  , assert $ sizeOf_ xs >=. lit 4
+  , assert $ sizeOf_ xs <=. lit 6
+  , assert $ elem_ (lit a) xs
+  ]
+
+-- ==============================================================
+-- Tools for building properties that have good counterexamples
+
+data Outcome = Succeed | Fail
+
+propYes :: String -> Solution t -> Property
+propYes _ (Yes _) = property True
+propYes msg (No xs) = property (counterexample (unlines (msg : xs)) False)
+
+propNo :: Show t => String -> Solution t -> Property
+propNo msg (Yes (x :| _)) = property (counterexample (unlines [msg, "Expected to fail, but succeeds with", show x]) False)
+propNo _ (No _) = property True
+
+parensList :: [String] -> String
+parensList xs = show (fillSep $ punctuate space $ map fromString xs)
+
+-- ===============================================================
+-- Functions for building properties about the functions defined
+-- in module Constrained.SumList(logish,pickAll)
+
+logishProp :: Gen Property
+logishProp = do
+  n <- choose (-17, 17 :: Int) -- Any bigger or smaller is out of the range of Int
+  i <- choose (logRange n)
+  pure (logish i === n)
+
+picktest :: (Ord a, Num a) => a -> (a -> Bool) -> a -> Int -> [a] -> Bool
+picktest smallest p total count ans =
+  total >= smallest
+    && total == sum ans
+    && count == length ans
+    && all p ans
+
+-- | generate a different category of test, each time.
+pickProp :: Gen Property
+pickProp = do
+  smallest <- elements [-4, 1 :: Int]
+  count <- choose (2, 4)
+  total <- (+ 20) <$> choose (smallest, 5477)
+  (nam, p) <-
+    elements
+      ( concat
+          [ if even total then [("even", even)] else []
+          , if odd total && odd count then [("odd", odd)] else []
+          , [("(>0)", (> 0)), ("true", const True)]
+          ]
+      )
+  (_cost, ans) <- pickAll smallest (nam, p) total count (Cost 0)
+  case ans of
+    Yes result -> pure $ property $ all (picktest smallest p total count) result
+    No msgs -> pure $ counterexample ("predicate " ++ nam ++ "\n" ++ unlines msgs) False
+
+-- | Build properties about calls to 'genListWithSize'
+testFoldSpec ::
+  forall a.
+  (Foldy BaseFn a, Random a, Integral a, TypeSpec BaseFn a ~ NumSpec BaseFn a) =>
+  Specification BaseFn Integer ->
+  Specification BaseFn a ->
+  Specification BaseFn a ->
+  Outcome ->
+  Gen Property
+testFoldSpec size elemSpec total outcome = do
+  ans <- genFromGenT $ inspect $ genListWithSize size elemSpec total
+  let callString = parensList ["GenListWithSize", show size, fst (predSpecPair elemSpec), show total]
+      fails xs = unlines [callString, "Should fail, but it succeeds with", show xs]
+      succeeds xs = unlines (callString : "Should succeed, but it fails with" : NE.toList xs)
+  case (ans, outcome) of
+    (Result _ _, Succeed) -> pure $ property True
+    (Result _ xs, Fail) -> pure $ counterexample (fails xs) False
+    (FatalError _ _, Fail) -> pure $ property True
+    (FatalError _ xs, Succeed) -> pure $ counterexample (succeeds xs) False
+    (GenError _ _, Fail) -> pure $ property True
+    (GenError _ xs, Succeed) -> pure $ counterexample (succeeds xs) False
+
+-- | Generate a property from a call to 'pickAll'. We can test for success or failure using 'outcome'
+sumProp ::
+  (Integral t, Random t, HasSpec BaseFn t) =>
+  t -> Specification BaseFn t -> t -> Int -> Outcome -> Gen Property
+sumProp smallest spec total count outcome = sumProp2 smallest (predSpecPair spec) total count outcome
+
+-- | Like SumProp, but instead of using a (Specification fn n) for the element predicate
+--   It uses an explicit pair of a (String, n -> Bool). This means we can test things
+--   using any Haskell function.
+sumProp2 ::
+  (Show t, Integral t, Random t) =>
+  t -> (String, t -> Bool) -> t -> Int -> Outcome -> Gen Property
+sumProp2 smallest spec total count outcome = do
+  (_, ans) <- pickAll smallest spec total count (Cost 0)
+  let callString = parensList ["pickAll", show smallest, (fst spec), show total, show count]
+      message Succeed = "\nShould succeed, but it fails with"
+      message Fail = "\nShould fail, but it succeeds with " ++ show ans
+  pure
+    ( case outcome of
+        Succeed -> propYes (callString ++ message outcome) ans
+        Fail -> propNo callString ans
+    )
diff --git a/libs/constrained-generators/src/Constrained/GenT.hs b/libs/constrained-generators/src/Constrained/GenT.hs
index bd9cc0fc2f3..fe52fa08608 100644
--- a/libs/constrained-generators/src/Constrained/GenT.hs
+++ b/libs/constrained-generators/src/Constrained/GenT.hs
@@ -110,7 +110,12 @@ fromGE _ (FatalError es e) =
   error . ("\n" ++) . unlines $ concat (map NE.toList es) ++ (NE.toList e)
 
 errorGE :: GE a -> a
-errorGE = fromGE (error . unlines . NE.toList)
+errorGE mge = case mge of
+  (FatalError xs x) -> error $ concat (map f (reverse (x : xs)))
+  (GenError xs x) -> error $ concat (map f (reverse (x : xs)))
+  (Result _ x) -> x
+  where
+    f x = unlines (NE.toList x) ++ "\n"
 
 isOk :: GE a -> Bool
 isOk GenError {} = False
diff --git a/libs/constrained-generators/src/Constrained/SumList.hs b/libs/constrained-generators/src/Constrained/SumList.hs
new file mode 100644
index 00000000000..7c2eca266f7
--- /dev/null
+++ b/libs/constrained-generators/src/Constrained/SumList.hs
@@ -0,0 +1,308 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Constrained.SumList where
+
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NE
+import System.Random (Random (..))
+import Test.QuickCheck (Gen, choose, shuffle, vectorOf)
+
+-- =======================================================
+-- Helper functions for genSizedList
+
+data Solution t = Yes (NonEmpty [t]) | No [String]
+  deriving (Eq)
+
+instance Show t => Show (Solution t) where
+  show (No xs) = "No" ++ "\n" ++ unlines xs
+  show (Yes xs) = "Yes " ++ show xs
+
+-- | Similar to (concat :: [[x]] -> [x]) for lists
+concatNE :: NonEmpty (NonEmpty t) -> NonEmpty t
+concatNE (x :| []) = x
+concatNE (x :| (y : ys)) = x <> concatNE (y :| ys)
+
+partitionNE :: [Solution t] -> ([NonEmpty [t]], [[String]])
+partitionNE xs = go xs ([], [])
+  where
+    go [] (ys, ns) = (reverse ys, reverse ns)
+    go (Yes y : more) (ys, ns) = go more (y : ys, ns)
+    go (No n : more) (ys, ns) = go more (ys, n : ns)
+
+concatSolution :: Show t => t -> String -> t -> Int -> [Solution t] -> Solution t
+concatSolution smallest pName total count sols = case partitionNE sols of
+  ([], n : _) -> No n -- All No
+  (y : ys, _) -> Yes $ concatNE (y :| ys) -- At least one Yes, and all No's skipped ('ys')
+  ([], []) ->
+    No -- The list is empty
+      [ "The sample in pickAll was empty"
+      , "smallest = " ++ show smallest
+      , "pred = " ++ pName
+      , "total = " ++ show total
+      , "count = " ++ show count
+      ]
+
+newtype Cost = Cost Int deriving (Eq, Show, Num, Ord)
+
+firstYesG ::
+  Monad m => Solution t -> (x -> Cost -> m (Cost, Solution t)) -> [x] -> Cost -> m (Cost, Solution t)
+firstYesG nullSolution f xs c = go xs c
+  where
+    go [] cost = pure (cost, nullSolution)
+    go [x] cost = f x (cost + 1)
+    go (x : more) cost = do
+      ans <- f x (cost + 1)
+      case ans of
+        (cost1, No _) -> go more cost1
+        (cost2, Yes y) -> pure (cost2, Yes y)
+
+noChoices :: Show t => Cost -> String -> t -> t -> Int -> [(t, t)] -> Solution t
+noChoices cost p smallest total count samp =
+  No
+    [ "No legal choice can be found, where"
+    , "  predicate = " ++ p
+    , "  smallest = " ++ show smallest
+    , "  total = " ++ show total
+    , "  count = " ++ show count
+    , "  cost = " ++ show cost
+    , "Small sample of what was explored"
+    , show samp
+    ]
+
+-- =====================================================
+
+{-# SPECIALIZE splitsOf :: Int -> [(Int, Int)] #-}
+
+-- | Given 'count', return a list if pairs, that add to 'count'
+--   splitsOf 6 --> [(1,5),(2,4),(3,3)].
+--   Note we don't return reflections like (5,1) and (4,2),
+--   as they have the same information as (1,5) and (2,4).
+splitsOf :: Integral b => b -> [(b, b)]
+splitsOf count = [(i, j) | i <- [1 .. div count 2], j <- [count - i]]
+
+{-# SPECIALIZE pickAll ::
+  Int -> (String, Int -> Bool) -> Int -> Int -> Cost -> Gen (Cost, Solution Int)
+  #-}
+
+-- | Given a Path, find a representative solution, 'ans', for that path, such that
+--   1) (length ans) == 'count',
+--   2) (sum ans) == 'total'
+--   3) (all p ans) is True
+--   What is a path?
+--   Suppose i==5, then we recursively explore every way to split 5 into
+--   split pairs that add to 5. I.e. (1,4) (2,3), then we split each of those.
+--   Here is a picture of the graph of all paths for i==5. A path goes from the root '5'
+--   to one of the leaves. Note all leaves are count == '1 (where the solution is '[total]').
+--   To solve for 5, we could solve either of the sub problems rooted at 5: [1,4] or [2,3].
+--   In 'pickAll' we will try to solve both, but in pick1, we only attempt 1 of those sub problems.
+--   5
+--   |
+--   [1,4]
+--   |  |
+--   |  [1,3]
+--   |  |  |
+--   |  |  [1,2]
+--   |  |     |
+--   |  |     [1,1]
+--   |  |
+--   |  [2,2]
+--   |   | |
+--   |   | [1,1]
+--   |   |
+--   |   [1,1]
+--   |
+--   [2,3]
+--    | |
+--    | [1,2]
+--    |    |
+--    |    [1,1]
+--    [1,1]
+--  In 'pickAll' will explore a path for every split of 'count'
+--  so if it returns (No _), we can be somewhat confidant that no solution exists.
+--  Note that count of 1 and 2, are base cases.
+--  When 'count' is greater than 1, we need to sample from [smallest..total],
+--  so 'smallest' better be less that or equal to 'total'
+pickAll ::
+  forall t.
+  (Show t, Integral t, Random t) =>
+  t -> (String, t -> Bool) -> t -> Int -> Cost -> Gen (Cost, Solution t)
+pickAll smallest (pName, _) total count cost
+  | cost > 1000 =
+      pure $
+        ( cost
+        , No
+            [ "pickAll exceeds cost limit " ++ show cost
+            , "  predicate = " ++ pName
+            , "  smallest = " ++ show smallest
+            , "  total = " ++ show total
+            , "  count = " ++ show count
+            ]
+        )
+pickAll smallest (pName, p) total 1 cost =
+  if p total
+    then pure $ (cost, Yes $ pure [total])
+    else pure $ (cost, noChoices cost pName smallest total 1 [(total, 0)])
+pickAll smallest (pName, _) total count cost
+  | smallest > total =
+      pure $
+        ( cost
+        , No
+            [ "The feasible range to pickAll [" ++ show smallest ++ " .. " ++ show (div total 2) ++ "] was empty"
+            , "  predicate = " ++ pName
+            , "  smallest = " ++ show smallest
+            , "  total = " ++ show total
+            , "  count = " ++ show count
+            , "  cost = " ++ show cost
+            ]
+        )
+pickAll smallest (pName, p) total 2 cost =
+  do
+    -- for small things, enumerate all possibilities
+    -- for large things, use a fair sample.
+    choices <- smallSample smallest total 1000 100
+    let goodChoices = filter (\(x, y) -> p x && p y) choices
+    case goodChoices of
+      [] -> pure $ (cost + 1, noChoices cost pName smallest total 2 (take 10 choices))
+      zs -> pure $ (cost + 1, Yes $ NE.fromList (fmap (\(x, y) -> [x, y]) zs))
+-- pickAll (11 - 10) (predSpecPair (leqSpec @BaseFn @Int (-6))) (-11) (fromInteger 21)
+pickAll smallest (pName, p) total count cost =
+  do
+    -- Compute a representative sample of the choices between smallest and total.
+    -- E.g. when smallest = -2, and total = 5, the complete set of values is:
+    -- [(-2,7),(-1,6),(0,5),(1,4),(2,3),(3,2),(4,1),(5,0)]  Note they all add to 5
+    -- We could explore the whole set of values, but that can be millions of choices.
+    -- so we choose to explore a representative subset. See the function 'fairSample', for details.
+    -- Remember this is just 1 step on one path. So if this step fails, there are many more
+    -- paths to explore. In fact there are usually many many solutions. We need to find just 1.
+    -- samp <- (fair smallest (div total 2) 500 3 True) >>= shuffle -- 12 is small, shuffle should be cheap
+    -- let choices = [(x, total - x) | x <- samp]
+    choices <- smallSample smallest total 1000 20
+    -- The choice of splits is crucial. If total >> count, we want the larger splits first
+    -- if count >> total , we want smaller splits first
+    splits <-
+      if count >= 20
+        then shuffle $ take 10 (splitsOf count)
+        else
+          if total > fromIntegral count
+            then pure (reverse (splitsOf count))
+            else pure (splitsOf count)
+
+    firstYesG
+      (No ["No split has a solution", "cost = " ++ show cost])
+      (doSplit smallest total (pName, p) choices (pickAll smallest))
+      splits
+      cost
+
+-- TODO run some tests to see if this is a better solution than firstYesG
+-- concatSolution smallest pName total count
+--  <$> mapM  (doSplit smallest total (pName, p) choices (pickAll (depth +1) smallest)) splits
+
+{-# INLINE doSplit #-}
+doSplit ::
+  (Show t, Integral t) =>
+  t ->
+  t ->
+  (String, t -> Bool) ->
+  [(t, t)] ->
+  ((String, t -> Bool) -> t -> Int -> Cost -> Gen (Cost, Solution t)) ->
+  (Int, Int) ->
+  Cost ->
+  Gen (Cost, Solution t)
+doSplit smallest total (pName, p) sample pick (i, j) c = go sample c
+  where
+    -- The 'sample' is a list of pairs (x,y), where we know (x+y) == total.
+    -- We will search for the first good solution in the given sample
+    -- to build a representative value for this path, with split (i,j).
+    go ((x, y) : more) cost0 = do
+      -- Note (i+j) = current length of the ans we are looking for
+      --      (x+y) = total
+      (cost1, ans1) <- pick (pName, p) x i cost0 -- pick 'ans1' such that (sum ans1 == x) and (length ans1 == i)
+      (cost2, ans2) <- pick (pName, p) y j cost1 -- pick 'ans2' such that (sum ans2 == y) and (length ans2 == j)
+      case (ans1, ans2) of
+        (Yes ys, Yes zs) -> pure $ (cost2, Yes (NE.fromList [a <> b | a <- NE.toList ys, b <- NE.toList zs]))
+        _ -> go more cost2
+    go [] cost =
+      case sample of
+        [] ->
+          pure $
+            ( cost
+            , No
+                [ "The sample passed to doSplit [" ++ show smallest ++ " .. " ++ show (div total 2) ++ "] was empty"
+                , "  predicate = " ++ pName
+                , "  smallest = " ++ show smallest
+                , "  total " ++ show total
+                , "  count = " ++ show (i + j)
+                , "  split of count = " ++ show (i, j)
+                ]
+            )
+        ((left, right) : _) ->
+          pure $
+            ( cost
+            , No
+                [ "All choices in (genSizedList " ++ show (i + j) ++ " 'p' " ++ show total ++ ") have failed."
+                , "Here is 1 example failure."
+                , "  smallest = " ++ show smallest
+                , "  total " ++ show total ++ " = " ++ show left ++ " + " ++ show right
+                , "  count = " ++ show (i + j) ++ ", split of count = " ++ show (i, j)
+                , "We are trying to solve sub-problems like:"
+                , "  split " ++ show left ++ " into " ++ show i ++ " parts, where all parts meet 'p'"
+                , "  split " ++ show right ++ " into " ++ show j ++ " parts, where all parts meet 'p'"
+                , "predicate 'p' = " ++ pName
+                , "prefix of the sample"
+                , unlines (map show (take 10 sample))
+                ]
+            )
+
+{-# INLINE smallSample #-}
+
+-- | If the sample is small enough, then enumerate all of it, otherwise take a fair sample.
+smallSample :: (Random t, Integral t) => t -> t -> t -> Int -> Gen [(t, t)]
+smallSample smallest total bound _size | total - smallest <= bound = do
+  choices <- shuffle $ takeWhile (uncurry (<=)) [(x, total - x) | x <- [smallest .. total]]
+  pure choices
+smallSample smallest total _bound size = do
+  choices <- fair smallest total size 5 True
+  shuffle [(x, total - x) | x <- choices]
+
+-- | Generates a fair sample of numbers between 'smallest' and 'largest'.
+--   makes sure there are numbers of all sizes. Controls both the size of the sample
+--   and the precision (how many powers of 10 are covered)
+--   Here is how we generate one sample when we call (fair (-3455) (10234) 12 3 True)
+--   raw = [(-9999,-1000),(-999,-100),(-99,-10),(-9,-1),(0,9),(10,99),(100,999),(1000,9999),(10000,99999)]
+--   ranges = [(-3455,-1000),(-999,-100),(-99,-10),(-9,-1),(0,9),(10,99),(100,999),(1000,9999),(10000,10234)]
+--   count = 4
+--   largePrecision = [(10000,10234),(1000,9999),(100,999)]
+--   smallPrecision = [(-3455,-1000),(-999,-100),(-99,-10)]
+--   answer generated = [10128,10104,10027,10048,4911,7821,5585,2157,448,630,802,889]
+fair :: (Random a, Integral a) => a -> a -> Int -> Int -> Bool -> Gen [a]
+fair smallest largest size precision isLarge =
+  concat <$> mapM oneRange (if isLarge then largePrecision else smallPrecision)
+  where
+    raw = map logRange [logish smallest .. logish largest]
+    fixEnds (x, y) = (max smallest x, min largest y)
+    ranges = map fixEnds raw
+    count = div size precision
+    largePrecision = take precision (reverse ranges)
+    smallPrecision = take precision ranges
+    oneRange (x, y) = vectorOf count (choose (x, y))
+
+logRange :: Integral a => a -> (a, a)
+logRange 1 = (10, 99)
+logRange (-1) = (-9, -1)
+logRange n = case compare n 0 of
+  EQ -> (0, 9)
+  LT -> (negate (div b 10), negate (div a 10))
+  GT -> (10 ^ n, 10 ^ (n + 1) - 1)
+  where
+    (a, b) = logRange (negate n)
+
+-- | like (logBase10 n), except negative answers mean negative numbers, rather than fractions less than 1.
+logish :: Integral t => t -> t
+logish n
+  | 0 <= n && n <= 9 = 0
+  | n > 9 = 1 + logish (n `div` 10)
+  | (-9) <= n && n <= (-1) = -1
+  | True = negate (1 + logish (negate n))
+
+-- =====================================================================
diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs
index 189fe50b581..e88b75a2278 100644
--- a/libs/constrained-generators/test/Constrained/Test.hs
+++ b/libs/constrained-generators/test/Constrained/Test.hs
@@ -14,8 +14,25 @@
 
 module Constrained.Test where
 
+import Constrained.Examples
+import Constrained.Examples.Fold (
+  Outcome (..),
+  evenSpec,
+  listSumComplex,
+  logishProp,
+  oddSpec,
+  pickProp,
+  sum3,
+  sum3WithLength,
+  sumProp,
+  sumProp2,
+  testFoldSpec,
+ )
+import Constrained.Internals
+import Constrained.Properties
 import Control.Monad
 import Data.Int
+import qualified Data.List.NonEmpty as NE
 import Data.Map (Map)
 import Data.Set (Set)
 import Data.Typeable
@@ -25,11 +42,6 @@ import Test.Hspec
 import Test.Hspec.QuickCheck
 import Test.QuickCheck hiding (Args, Fun, forAll)
 
-import Constrained.Examples
-import Constrained.Internals
-import Constrained.Properties
-import qualified Data.List.NonEmpty as NE
-
 ------------------------------------------------------------------------
 -- Test suite
 ------------------------------------------------------------------------
@@ -185,6 +197,7 @@ tests nightly =
     negativeTests
     prop "prop_noNarrowLoop" $ withMaxSuccess 1000 prop_noNarrowLoop
     conformsToSpecESpec
+    foldWithSizeTests
 
 negativeTests :: Spec
 negativeTests =
@@ -412,3 +425,46 @@ conformsToSpecESpec =
       prop "Set Integer" (conformsToSpecETest @(Set Integer))
       prop "Set[Int]" (conformsToSpecETest @(Set [Int]))
       prop "Map Int Int" (conformsToSpecETest @(Map Int Int))
+
+-- ======================================================================
+-- Test for use of Fold with size annotations
+
+foldWithSizeTests :: Spec
+foldWithSizeTests = do
+  describe "Summation tests with size. " $ do
+    prop "logish is sound" logishProp
+    prop "small odd/even tests" pickProp
+    prop "negative small" $ sumProp (-1000) TrueSpec (-400 :: Int) 4 Succeed
+    prop "negative sum too small" $ sumProp (-1000) TrueSpec (-8002 :: Int) 4 Fail
+    prop "negative large" $ sumProp (-60000 :: Int) TrueSpec (-1000) 4 Succeed
+    prop "(between 50 60) small enough" $ sumProp 1 (between @BaseFn 50 60) (200 :: Int) 4 Succeed
+    prop "(between 50 60) too large" $ sumProp 1 (between @BaseFn 50 60) (400 :: Int) 4 Fail
+    prop "(count 2) large is fast" $ sumProp 1 TrueSpec (5000000 :: Int) 2 Succeed
+    prop "(count 5) large is fast" $ sumProp 1 TrueSpec (5000000 :: Int) 5 Succeed
+    prop "even succeeds on even" $ sumProp2 1 ("even", even) (45876 :: Int) 5 Succeed
+    prop "even succeeds on even spec" $ sumProp 1 evenSpec (45876 :: Int) 5 Succeed
+    prop "even fails on odd total, odd count" $ sumProp 1 evenSpec (45875 :: Int) 3 Fail
+    prop "odd fails on odd total, even count" $ sumProp 1 oddSpec (45878 :: Int) 3 Fail
+    prop "odd succeeds on odd total, odd count" $ sumProp 1 oddSpec (45871 :: Int) 3 Succeed
+    xprop "succeeds with large count" $
+      withMaxSuccess 100 (sumProp 1 TrueSpec (1500567 :: Int) 20 Succeed)
+    prop "sum3 is sound" $ prop_constrained_satisfies_sound sum3
+    prop "(sum3WithLength 3) is sound" $ prop_constrained_satisfies_sound (sum3WithLength 3)
+    prop "(sum3WithLength 4) is sound" $ prop_constrained_satisfies_sound (sum3WithLength 4)
+    prop "(sum3WithLength 7) is sound" $ prop_constrained_satisfies_sound (sum3WithLength 7)
+    prop "listSum is sound" $ prop_constrained_satisfies_sound (listSum @Int)
+    prop "listSumPair is sound" $ prop_constrained_satisfies_sound (listSumPair @Word64)
+    -- This, by design, will fail for inputs greater than 7
+    prop "listSumComplex is sound" $ prop_constrained_satisfies_sound (listSumComplex @Integer 7)
+    prop "All sizes are negative" $
+      testFoldSpec @Int (between (-5) (-2)) evenSpec (MemberSpec (pure 100)) Fail
+    prop "Only some sizes are negative" $
+      testFoldSpec @Int (between (-5) 0) evenSpec (MemberSpec (pure 100)) Fail
+    prop "total and count can only be 0 in Word type" $
+      testFoldSpec @Word64 (between 0 0) evenSpec (MemberSpec (pure 0)) Succeed
+    prop "something of size 2, can add to 0" $
+      testFoldSpec @Int (between 2 2) evenSpec (MemberSpec (pure 0)) Succeed
+    prop "TEST listSum" $ prop_constrained_satisfies_sound (listSum @Int)
+
+-- TODO Needs to sample like this: OR [pick t c | t <- total, c <- count]
+-- prop "count =0, total is 0,1,2" $ testFoldSpec @Int (between 0 1) evenSpec (between 0 2) Succeed