From 52aa3490c7f132a4f2b0c23d89e6f42193d7a714 Mon Sep 17 00:00:00 2001
From: Tim Sheard <sheard@pdx.edu>
Date: Sun, 5 Jan 2025 19:26:57 -0800
Subject: [PATCH 1/2] 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

---
 libs/constrained-generators/src/Constrained/Base.hs    | 2 +-
 libs/constrained-generators/src/Constrained/SumList.hs | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
index 67fa8941877..3527ec28fa7 100644
--- a/libs/constrained-generators/src/Constrained/Base.hs
+++ b/libs/constrained-generators/src/Constrained/Base.hs
@@ -5636,7 +5636,7 @@ showType :: forall t. Typeable t => String
 showType = show (typeRep (Proxy @t))
 
 prettyType :: forall t x. Typeable t => Doc x
-prettyType = fromString $ showType @t
+prettyType = fromString $ show (typeRep (Proxy @t))
 
 instance HasSpec fn a => Pretty (Term fn a) where
   pretty = prettyPrec 0
diff --git a/libs/constrained-generators/src/Constrained/SumList.hs b/libs/constrained-generators/src/Constrained/SumList.hs
index d99405c0cda..ec7b1d64b6c 100644
--- a/libs/constrained-generators/src/Constrained/SumList.hs
+++ b/libs/constrained-generators/src/Constrained/SumList.hs
@@ -55,6 +55,7 @@ firstYesG nullSolution f xs c = go xs c
       ans <- f x (cost + 1)
       case ans of
         (cost1, No _) -> go more cost1
+        (cost2, Yes y) -> pure (cost2, Yes y)
         _ -> pure ans
 
 noChoices :: Show t => Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
@@ -73,6 +74,7 @@ noChoices cost p smallest largest total count samp =
 
 -- =====================================================
 
+
 -- | 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),
@@ -81,6 +83,7 @@ splitsOf :: Integral b => b -> [(b, b)]
 splitsOf count = [(i, j) | i <- [1 .. div count 2], let j = count - i]
 {-# SPECIALIZE splitsOf :: Int -> [(Int, Int)] #-}
 
+
 -- | Given a Path, find a representative solution, 'ans', for that path, such that
 --   1) (length ans) == 'count',
 --   2) (sum ans) == 'total'
@@ -186,6 +189,7 @@ pickAll smallest largest (pName, p) total count cost = do
     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
@@ -249,6 +253,7 @@ doSplit smallest largest (pName, p) total sample (i, j) c = go sample c
                 , unlines (map show (take 10 sample))
                 ]
             )
+
 {-# INLINE doSplit #-}
 
 -- | If the sample is small enough, then enumerate all of it, otherwise take a fair sample.
@@ -261,6 +266,7 @@ smallSample smallest largest total bound size
       shuffle [(x, total - x) | x <- choices]
 {-# INLINE smallSample #-}
 
+
 -- | 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)

From 84671a09fb03c5c0dc4d43cb95c205dc5122e419 Mon Sep 17 00:00:00 2001
From: Tim Sheard <sheard@pdx.edu>
Date: Thu, 16 Jan 2025 22:29:36 -0800
Subject: [PATCH 2/2] Changed the monad in Constrained.GenT to use reader
 instead of state.

---
 .../Ledger/Conformance/ExecSpecRule/Core.hs   |   6 +-
 .../src/Constrained/Base.hs                   |  45 +--
 .../src/Constrained/Examples/Fold.hs          |  16 +-
 .../src/Constrained/GenT.hs                   | 340 ++++++++++--------
 .../src/Constrained/Properties.hs             |   2 +-
 .../src/Constrained/SumList.hs                |  52 +--
 6 files changed, 260 insertions(+), 201 deletions(-)

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs
index bd371c9e72c..723a381f530 100644
--- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs
+++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs
@@ -428,13 +428,13 @@ conformsToImpl = property @(ImpTestM era Property) . (`runContT` pure) $ do
     forAllSpec spec = do
       let
         simplifiedSpec = simplifySpec spec
-        generator = CV2.runGenT (CV2.genFromSpecT simplifiedSpec) Loose
-        shrinker (Result _ x) = pure <$> shrinkWithSpec simplifiedSpec x
+        generator = CV2.runGenT (CV2.genFromSpecT simplifiedSpec) Loose []
+        shrinker (Result x) = pure <$> shrinkWithSpec simplifiedSpec x
         shrinker _ = []
       res :: GE a <- ContT $ \c ->
         pure $ forAllShrinkBlind generator shrinker c
       case res of
-        Result _ x -> pure x
+        Result x -> pure x
         _ -> ContT . const . pure $ property Discard
   env <- forAllSpec $ environmentSpec @fn @rule @era ctx
   deepEval env "environment"
diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
index 3527ec28fa7..c62f5db5743 100644
--- a/libs/constrained-generators/src/Constrained/Base.hs
+++ b/libs/constrained-generators/src/Constrained/Base.hs
@@ -74,7 +74,7 @@ import GHC.Natural
 import GHC.Real
 import GHC.Stack
 import GHC.TypeLits
-import Prettyprinter
+import Prettyprinter hiding (cat)
 import System.Random
 import System.Random.Stateful
 import Test.QuickCheck hiding (Args, Fun, forAll)
@@ -532,7 +532,7 @@ monitorPred env = \case
     monitorPred (extendEnv x val env) p
   Exists k (x :-> p) -> do
     case k (errorGE . explain1 "monitorPred: Exists" . runTerm env) of
-      Result _ a -> monitorPred (extendEnv x a env) p
+      Result a -> monitorPred (extendEnv x a env) p
       _ -> pure id
   Explain es p -> explain es $ monitorPred env p
 
@@ -787,7 +787,7 @@ instance (HasSpec fn a, Arbitrary (TypeSpec fn a)) => Arbitrary (Specification f
   shrink (SuspendedSpec x p) =
     [TrueSpec, ErrorSpec (pure "From shrinking SuspendedSpec")]
       ++ [ s
-         | Result _ s <- [computeSpec x p]
+         | Result s <- [computeSpec x p]
          , not $ isSuspendedSpec s
          ]
       ++ [SuspendedSpec x p' | p' <- shrinkPred p]
@@ -1167,8 +1167,7 @@ genFromSpecT (simplifySpec -> spec) = case spec of
           [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a
           , "tspec = "
           , show s
-          , "cant = "
-          , unlines (map (\x -> "  " ++ show x) cant)
+          , "cant = " ++ show (short cant)
           , "with mode " ++ show mode
           ]
       )
@@ -1196,7 +1195,7 @@ shrinkWithSpec (simplifySpec -> spec) a = filter (`conformsToSpec` spec) $ case
 
 shrinkFromPreds :: HasSpec fn a => Pred fn -> Var a -> a -> [a]
 shrinkFromPreds p
-  | Result _ plan <- prepareLinearization p = \x a -> listFromGE $ do
+  | Result plan <- prepareLinearization p = \x a -> listFromGE $ do
       -- NOTE: we do this to e.g. guard against bad construction functions in Exists
       xaGood <- checkPred (singletonEnv x a) p
       unless xaGood $
@@ -1292,7 +1291,7 @@ envFromPred env p = case p of
 genFromSpec :: forall fn a. (HasCallStack, HasSpec fn a) => Specification fn a -> Gen a
 genFromSpec spec = do
   res <- catchGen $ genFromSpecT @fn @a @GE spec
-  either (error . show . NE.toList) pure res
+  either (error . show . catMessages) pure res
 
 -- | A version of `genFromSpecT` that takes a seed and a size and gives you a result
 genFromSpecWithSeed ::
@@ -1309,9 +1308,9 @@ debugSpec spec = do
           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
+    FatalError xs -> mapM_ f xs
+    GenError xs -> mapM_ f xs
+    Result x -> print spec >> print x >> ok x
 
 genInverse ::
   ( MonadGenError m
@@ -1519,7 +1518,7 @@ backPropagation (SolverPlan plan graph) = SolverPlan (go [] (reverse plan)) grap
         termVarEqCases spec x' t
           | Just Refl <- eqVar x x'
           , [Name y] <- Set.toList $ freeVarSet t
-          , Result _ ctx <- toCtx y t =
+          , Result ctx <- toCtx y t =
               [SolverStage y [] (propagateSpec spec ctx)]
         termVarEqCases _ _ _ = []
 
@@ -1608,7 +1607,7 @@ short xs = "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <
 prettyPlan :: HasSpec fn a => Specification fn a -> Doc ann
 prettyPlan (simplifySpec -> spec)
   | SuspendedSpec _ p <- spec
-  , Result _ plan <- prepareLinearization p =
+  , Result plan <- prepareLinearization p =
       vsep'
         [ "Simplified spec:" /> pretty spec
         , pretty plan
@@ -1761,9 +1760,9 @@ normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec'
 
 fromGESpec :: HasCallStack => GE (Specification fn a) -> Specification fn a
 fromGESpec ge = case ge of
-  Result [] s -> s
-  Result es s -> addToErrorSpec (foldr1 (<>) es) s
-  _ -> fromGE ErrorSpec ge
+  Result s -> s
+  GenError xs -> ErrorSpec (catMessageList xs)
+  FatalError es -> error $ catMessages es
 
 -- | Add the explanations, if it's an ErrorSpec, else drop them
 addToErrorSpec :: NE.NonEmpty String -> Specification fn a -> Specification fn a
@@ -1886,8 +1885,10 @@ computeSpecSimplified x p = localGESpec $ case p of
         ["The impossible happened in computeSpec: Reifies", "  " ++ show x, show $ indent 2 (pretty p)]
   where
     -- We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError`
-    localGESpec ge@FatalError {} = ge
-    localGESpec ge = pure $ fromGESpec ge
+    localGESpec ge = case ge of
+      (GenError xs) -> Result $ ErrorSpec (catMessageList xs)
+      (FatalError es) -> FatalError es
+      (Result x) -> Result x
 
 -- | Precondition: the `Pred fn` defines the `Var a`.
 --
@@ -6236,11 +6237,13 @@ checkPredE env msgs = \case
           Right v -> v
           Left es -> error $ unlines $ NE.toList (msgs <> es)
      in case k eval of
-          Result _ a -> checkPredE (extendEnv x a env) msgs p
-          FatalError ess es -> Just (msgs <> foldr1 (<>) ess <> es)
-          GenError ess es -> Just (msgs <> foldr1 (<>) ess <> es)
+          Result a -> checkPredE (extendEnv x a env) msgs p
+          FatalError es -> Just (msgs <> catMessageList es)
+          GenError es -> Just (msgs <> catMessageList es)
   Explain es p -> checkPredE env (msgs <> es) p
 
+-- | conformsToSpec with explanation. Nothing if (conformsToSpec a spec),
+--   but (Just explanations) if not(conformsToSpec a spec).
 conformsToSpecE ::
   forall fn a.
   HasSpec fn a =>
@@ -6249,7 +6252,7 @@ conformsToSpecE ::
   NE.NonEmpty String ->
   Maybe (NE.NonEmpty String)
 conformsToSpecE a (ExplainSpec [] s) msgs = conformsToSpecE a s msgs
-conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s (msgs <> (x NE.:| xs))
+conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s ((x :| xs) <> msgs)
 conformsToSpecE _ TrueSpec _ = Nothing
 conformsToSpecE a (MemberSpec as) msgs =
   if elem a as
diff --git a/libs/constrained-generators/src/Constrained/Examples/Fold.hs b/libs/constrained-generators/src/Constrained/Examples/Fold.hs
index 61f6797f7c6..b8298106b1a 100644
--- a/libs/constrained-generators/src/Constrained/Examples/Fold.hs
+++ b/libs/constrained-generators/src/Constrained/Examples/Fold.hs
@@ -14,7 +14,6 @@ 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)
@@ -141,14 +140,15 @@ 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)
+      succeeds xs =
+        unlines [callString, "Should succeed, but it fails with", catMessages 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
+    (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 ::
diff --git a/libs/constrained-generators/src/Constrained/GenT.hs b/libs/constrained-generators/src/Constrained/GenT.hs
index a8fb3a95762..c7260a3dee7 100644
--- a/libs/constrained-generators/src/Constrained/GenT.hs
+++ b/libs/constrained-generators/src/Constrained/GenT.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
@@ -31,24 +32,79 @@ module Constrained.GenT where
 
 import Control.Monad
 import Data.Foldable
+import Data.List.NonEmpty (NonEmpty ((:|)), (<|))
 import Data.List.NonEmpty qualified as NE
 import GHC.Stack
 import System.Random
 import Test.QuickCheck hiding (Args, Fun)
 import Test.QuickCheck.Gen
-import Test.QuickCheck.Random
 
+-- ==============================================================
+-- The GE Monad
+
+-- | It distinguishes between two kinds of errors: FatalError and GenError
+-- and non-fatal errors.
+data GE a
+  = FatalError (NonEmpty (NonEmpty String))
+  | GenError (NonEmpty (NonEmpty String))
+  | Result a
+  deriving (Ord, Eq, Show, Functor)
+
+instance Applicative GE where
+  pure = Result
+  (<*>) = ap
+
+instance Monad GE where
+  FatalError es >>= _ = FatalError es
+  GenError es >>= _ = GenError es
+  Result a >>= k = k a
+
+------------------------------------------------------------------------
+-- The GenT monad
+-- An environment monad on top of GE
 ------------------------------------------------------------------------
--- The Gen Error monad
+
+-- | Generation mode - how strict are we about requiring the generator to
+-- succeed. This is necessary because sometimes failing to find a value means
+-- there is an actual problem (a generator _should_ be satisfiable but for
+-- whatever buggy reason it isn't) and sometimes failing to find a value just
+-- means there are no values. The latter case is very relevant when you're
+-- generating e.g. lists or sets of values that can be empty.
+data GenMode
+  = Loose
+  | Strict
+  deriving (Ord, Eq, Show)
+
+newtype GenT m a = GenT {runGenT :: GenMode -> [NonEmpty String] -> Gen (m a)}
+  deriving (Functor)
+
+instance Monad m => Applicative (GenT m) where
+  pure a = GenT (\_ _ -> pure @Gen (pure @m a))
+  (<*>) = ap
+
+-- I think this might be an inlined use of the Gen monad transformer?
+instance Monad m => Monad (GenT m) where
+  GenT m >>= k = GenT $ \mode -> \msgs -> MkGen $ \r n -> do
+    let (r1, r2) = split r
+    a <- unGen (m mode msgs) r1 n
+    unGen (runGenT (k a) mode msgs) r2 n
+
+instance MonadGenError m => MonadFail (GenT m) where
+  fail s = genError (pure s)
+
 ------------------------------------------------------------------------
+-- The MonadGenError transformer
+----------------------------------------------------------------------
 
 -- | A class for different types of errors with a stack of `explain` calls to
--- narrow down problems. The (NE.NonEmpty String) means one cannot cause an
+-- narrow down problems. The (NonEmpty String) means one cannot cause an
 -- Error without at least 1 string to explain it.
 class Monad m => MonadGenError m where
-  genError :: HasCallStack => NE.NonEmpty String -> m a
-  fatalError :: HasCallStack => NE.NonEmpty String -> m a
-  explain :: HasCallStack => NE.NonEmpty String -> m a -> m a
+  genError :: HasCallStack => NonEmpty String -> m a
+  fatalError :: HasCallStack => NonEmpty String -> m a
+  genErrors :: HasCallStack => NonEmpty (NonEmpty String) -> m a
+  fatalErrors :: HasCallStack => NonEmpty (NonEmpty String) -> m a
+  explain :: HasCallStack => NonEmpty String -> m a -> m a
 
 -- | genError with one line of explanation
 genError1 :: MonadGenError m => String -> m a
@@ -62,82 +118,107 @@ fatalError1 s = fatalError (pure s)
 explain1 :: MonadGenError m => String -> m a -> m a
 explain1 s = explain (pure s)
 
--- | The Gen Error monad, distinguishes between fatal errors
--- and non-fatal errors.
-data GE a
-  = FatalError [NE.NonEmpty String] (NE.NonEmpty String)
-  | GenError [NE.NonEmpty String] (NE.NonEmpty String)
-  | Result [NE.NonEmpty String] a
-  deriving (Ord, Eq, Show, Functor)
-
-instance Applicative GE where
-  pure = Result []
-  (<*>) = ap
-
-instance Monad GE where
-  FatalError es err >>= _ = FatalError es err
-  GenError es err >>= _ = GenError es err
-  Result _ a >>= k = k a
+-- GE instance
 
 instance MonadGenError GE where
-  genError neStr = GenError [] neStr
-  fatalError neStr = FatalError [] neStr
-  explain nes ge = case ge of
-    GenError es' err -> GenError (nes : es') err
-    FatalError es' err -> FatalError (nes : es') err
-    Result es' a -> Result (nes : es') a
+  genError msg = GenError (pure msg)
+  genErrors msgs = GenError msgs
+  fatalError msg = FatalError (pure msg)
+  fatalErrors msgs = FatalError msgs
+  explain m (GenError ms) = GenError (m <| ms)
+  explain m (FatalError ms) = FatalError (m <| ms)
+  explain _ (Result x) = Result x
 
+-- GenT instance
+
+-- | calls to genError and fatalError, add the stacked messages in the monad.
 instance MonadGenError m => MonadGenError (GenT m) where
-  genError es = GenT $ \_ -> pure $ genError es
-  fatalError es = GenT $ \_ -> pure $ fatalError es
-  explain es gen = GenT $ \mode -> fmap (explain es) (runGenT gen mode)
+  genError e = GenT $ \_ xs -> pure $ genErrors (add e xs)
+  genErrors es = GenT $ \_ xs -> pure $ genErrors (cat es xs)
 
-instance MonadGenError m => MonadFail (GenT m) where
-  fail s = genError (pure s)
+  -- Perhaps we want to turn genError into fatalError, if mode_ is Strict?
+  fatalError e = GenT $ \_ xs -> pure $ fatalErrors (add e xs)
+  fatalErrors es = GenT $ \_ xs -> pure $ fatalErrors (cat es xs)
 
-catGEs :: MonadGenError m => [GE a] -> m [a]
-catGEs [] = pure []
-catGEs (Result _ a : ges) = (a :) <$> catGEs ges
-catGEs (GenError {} : ges) = catGEs ges
-catGEs (FatalError es e : _) =
-  runGE $ FatalError es e
+  -- Perhaps we want to turn fatalError into genError, if mode_ is Loose?
+  explain e (GenT f) = GenT $ \mode es -> fmap (explain e) (f mode es)
 
-fromGE :: (NE.NonEmpty String -> a) -> GE a -> a
-fromGE _ (Result _ a) = a
-fromGE a (GenError [] e) = a e
-fromGE a (GenError es e) = a $ foldr1 (<>) es <> e
-fromGE _ (FatalError es e) =
-  error . ("\n" ++) . unlines $ concat (map NE.toList es) ++ (NE.toList e)
+-- ====================================================
+-- useful operations on NonEmpty
 
-errorGE :: GE a -> a
-errorGE mge = case mge of
-  FatalError xs x -> error $ mkErrorMsg xs x
-  GenError xs x -> error $ mkErrorMsg xs x
-  Result _ x -> x
+add :: NonEmpty a -> [NonEmpty a] -> NonEmpty (NonEmpty a)
+add a [] = pure a
+add a (x : xs) = a <| (x :| xs)
+
+cat :: NonEmpty (NonEmpty a) -> [NonEmpty a] -> NonEmpty (NonEmpty a)
+cat a [] = a
+cat a (x : xs) = a <> (x :| xs)
+
+-- | Sometimes we have a bunch of genError or fatalError
+--   messages we want to combine into one big message.
+--   This happens when we want to lift one of these into an input for 'error'
+catMessages :: NonEmpty (NonEmpty String) -> String
+catMessages xs = unlines (NE.toList (catMessageList xs))
+
+-- | Turn each inner (NonEmpty String) into a String
+catMessageList :: NonEmpty (NonEmpty String) -> NonEmpty String
+catMessageList = fmap (unlines . NE.toList)
+
+-- ========================================================
+-- Useful operations on GE
+
+-- If none of the GE's are FatalError, then concat together all the
+-- Result's (skipping over GenError). If there is at least one
+-- (FatalError xs) abort, and lift all those 'xs' as errors in the monad 'm'
+catGEs :: forall m a. MonadGenError m => [GE a] -> m [a]
+catGEs ges0 = go [] ges0
   where
-    mkErrorMsg xs x = concatMap f (reverse (x : xs))
-    f x = unlines (NE.toList x) ++ "\n"
+    go acc [] = pure $ reverse acc
+    go !acc (g : ges) =
+      case g of
+        Result a -> go (a : acc) ges
+        GenError _ -> go acc ges
+        FatalError xs -> fatalErrors xs
+
+-- | Given a function for handling GenError,
+--   and handling FatalError by using 'error'
+--   Turn (GE a) into 'a'
+fromGE :: HasCallStack => (NonEmpty (NonEmpty String) -> a) -> GE a -> a
+fromGE f ge = case ge of
+  Result a -> a
+  GenError xs -> f xs
+  FatalError es -> error $ catMessages es
+
+-- | Turn (GE a) into a
+--   both GenError and FatalErrors are handled by using 'error'
+errorGE :: GE a -> a
+errorGE ge = case ge of
+  FatalError xs -> error $ catMessages xs
+  GenError xs -> error $ catMessages xs
+  Result x -> x
 
 isOk :: GE a -> Bool
-isOk GenError {} = False
-isOk FatalError {} = False
-isOk Result {} = True
+isOk ge = case ge of
+  GenError {} -> False
+  FatalError {} -> False
+  Result {} -> True
 
-runGE :: MonadGenError m => GE r -> m r
-runGE (GenError es err) = foldr explain (genError err) es
-runGE (FatalError es err) = foldr explain (fatalError err) es
-runGE (Result es a) = foldr explain (pure a) es
+runGE :: forall m r. MonadGenError m => GE r -> m r
+runGE ge = case ge of
+  GenError es -> genErrors es
+  FatalError es -> fatalErrors es
+  Result a -> pure a
 
 fromGEProp :: Testable p => GE p -> Property
-fromGEProp (GenError es err) =
-  foldr (counterexample . unlines) (counterexample (unlines (NE.toList err)) False) (map NE.toList es)
-fromGEProp (FatalError es err) =
-  foldr (counterexample . unlines) (counterexample (unlines (NE.toList err)) False) (map NE.toList es)
-fromGEProp (Result es p) = foldr (counterexample . unlines) (property p) (map NE.toList es)
+fromGEProp ge = case ge of
+  GenError es -> counterexample (catMessages es) False
+  FatalError es -> counterexample (catMessages es) False
+  Result p -> property p
 
 fromGEDiscard :: Testable p => GE p -> Property
-fromGEDiscard (Result es p) = foldr (counterexample . unlines . NE.toList) (property p) es
-fromGEDiscard _ = discard
+fromGEDiscard ge = case ge of
+  Result p -> property p
+  _ -> discard
 
 headGE :: Foldable t => t a -> GE a
 headGE t
@@ -148,50 +229,24 @@ headGE t
 listFromGE :: GE [a] -> [a]
 listFromGE = fromGE (const []) . explain1 "listFromGE"
 
-------------------------------------------------------------------------
--- GenT
-------------------------------------------------------------------------
-
--- | Generation mode - how strict are we about requiring the generator to
--- succeed. This is necessary because sometimes failing to find a value means
--- there is an actual problem (a generator _should_ be satisfiable but for
--- whatever buggy reason it isn't) and sometimes failing to find a value just
--- means there are no values. The latter case is very relevant when you're
--- generating e.g. lists or sets of values that can be empty.
-data GenMode
-  = Loose
-  | Strict
-  deriving (Ord, Eq, Show)
-
--- TODO: put a global suchThat fuel parameter in here? To avoid exponential blowup of nested such
--- thats?
-newtype GenT m a = GenT {runGenT :: GenMode -> Gen (m a)}
-  deriving (Functor)
-
-instance Monad m => Applicative (GenT m) where
-  pure x = GenT $ \_ -> pure (pure x)
-  (<*>) = ap
-
-instance Monad m => Monad (GenT m) where
-  GenT m >>= k = GenT $ \mode -> MkGen $ \r n -> do
-    a <- unGen (m mode) (left r) n
-    unGen (runGenT (k a) mode) (right r) n
+-- ========================================================
+-- Useful operations on GenT
 
 strictGen :: GenT m a -> Gen (m a)
-strictGen gen = runGenT gen Strict
+strictGen genT = runGenT genT Strict []
 
 genFromGenT :: GenT GE a -> Gen a
-genFromGenT genT = errorGE <$> runGenT genT Strict
+genFromGenT genT = errorGE <$> runGenT genT Strict []
 
 resizeT :: (Int -> Int) -> GenT m a -> GenT m a
-resizeT f (GenT gm) = GenT $ \mode -> sized $ \sz -> resize (f sz) (gm mode)
+resizeT f (GenT gm) = GenT $ \mode msgs -> sized $ \sz -> resize (f sz) (gm mode msgs)
 
 pureGen :: Applicative m => Gen a -> GenT m a
-pureGen gen = GenT $ \_ -> pure <$> gen
+pureGen gen = GenT $ \_ _ -> pure <$> gen
 
 listOfT :: MonadGenError m => GenT GE a -> GenT m [a]
 listOfT gen = do
-  lst <- pureGen . listOf $ runGenT gen Loose
+  lst <- pureGen . listOf $ runGenT gen Loose []
   catGEs lst
 
 -- | Generate a list of elements of length at most `goalLen`, but accepting failure
@@ -203,16 +258,16 @@ listOfUntilLenT gen goalLen validLen =
   genList `suchThatT` validLen . length
   where
     genList = do
-      res <- pureGen . vectorOf goalLen $ runGenT gen Loose
+      res <- pureGen . vectorOf goalLen $ runGenT gen Loose []
       catGEs res
 
 vectorOfT :: MonadGenError m => Int -> GenT GE a -> GenT m [a]
-vectorOfT i gen = GenT $ \mode -> do
-  res <- fmap sequence . vectorOf i $ runGenT gen Strict
+vectorOfT i gen = GenT $ \mode _ -> do
+  res <- fmap sequence . vectorOf i $ runGenT gen Strict []
   case mode of
     Strict -> pure $ runGE res
     Loose -> case res of
-      FatalError es e -> pure $ runGE (GenError es e)
+      FatalError es -> pure $ genErrors es
       _ -> pure $ runGE res
 
 infixl 2 `suchThatT`
@@ -233,28 +288,33 @@ suchThatWithTryT tries g p = do
       if p a then pure a else scaleT (+ 1) $ go (n - 1) cont
 
 scaleT :: (Int -> Int) -> GenT m a -> GenT m a
-scaleT sc (GenT gen) = GenT $ \mode -> scale sc $ gen mode
+scaleT sc (GenT gen) = GenT $ \mode msgs -> scale sc $ gen mode msgs
 
 getMode :: Applicative m => GenT m GenMode
-getMode = GenT $ \mode -> pure (pure mode)
+getMode = GenT $ \mode _ -> pure (pure mode)
+
+getMessages :: Applicative m => GenT m [NonEmpty String]
+getMessages = GenT $ \_ msgs -> pure (pure msgs)
 
 withMode :: GenMode -> GenT m a -> GenT m a
-withMode mode gen = GenT $ \_ -> runGenT gen mode
+withMode mode gen = GenT $ \_ msgs -> runGenT gen mode msgs
 
 oneofT :: MonadGenError m => [GenT GE a] -> GenT m a
 oneofT gs = do
   mode <- getMode
+  msgs <- getMessages
   r <-
     explain (pure "suchThatT in oneofT") $
-      pureGen (oneof [runGenT g mode | g <- gs]) `suchThatT` isOk
+      pureGen (oneof [runGenT g mode msgs | g <- gs]) `suchThatT` isOk
   runGE r
 
 frequencyT :: MonadGenError m => [(Int, GenT GE a)] -> GenT m a
 frequencyT gs = do
   mode <- getMode
+  msgs <- getMessages
   r <-
     explain (pure "suchThatT in oneofT") $
-      pureGen (frequency [(f, runGenT g mode) | (f, g) <- gs]) `suchThatT` isOk
+      pureGen (frequency [(f, runGenT g mode msgs) | (f, g) <- gs]) `suchThatT` isOk
   runGE r
 
 chooseT :: (Random a, Ord a, Show a, MonadGenError m) => (a, a) -> GenT m a
@@ -263,7 +323,7 @@ chooseT (a, b)
   | otherwise = pureGen $ choose (a, b)
 
 sizeT :: Monad m => GenT m Int
-sizeT = GenT $ \mode -> sized $ \n -> runGenT (pure n) mode
+sizeT = GenT $ \mode msgs -> sized $ \n -> runGenT (pure n) mode msgs
 
 -- ==================================================================
 -- Reflective analysis of the internal GE structure of (GenT GE x)
@@ -274,36 +334,38 @@ sizeT = GenT $ \mode -> sized $ \n -> runGenT (pure n) mode
 inspect :: forall m x. MonadGenError m => GenT GE x -> GenT m (GE x)
 inspect (GenT f) = GenT g
   where
-    g mode = do result <- f mode; pure @Gen (pure @m result)
+    g mode msgs = do geThing <- f mode msgs; pure @Gen (pure @m geThing)
 
 -- | Ignore all kinds of Errors, by squashing them into Nothing
 tryGenT :: MonadGenError m => GenT GE a -> GenT m (Maybe a)
 tryGenT g = do
   r <- inspect g
   case r of
-    FatalError _ _ -> pure Nothing
-    GenError _ _ -> pure Nothing
-    Result es a -> explain (foldr1 (<>) es) (pure $ Just a)
+    FatalError _ -> pure Nothing
+    GenError _ -> pure Nothing
+    Result a -> pure $ Just a
 
 -- Pass on the error messages of both kinds of Errors, by squashing and combining both of them into Left constructor
-catchGenT :: MonadGenError m => GenT GE a -> GenT m (Either (NE.NonEmpty String) a)
+catchGenT :: MonadGenError m => GenT GE a -> GenT m (Either (NonEmpty (NonEmpty String)) a)
 catchGenT g = do
   r <- inspect g
   case r of
-    FatalError es e -> pure $ Left (foldr1 (<>) es <> e)
-    GenError es e -> pure $ Left (foldr1 (<>) es <> e)
-    Result es a -> explain (foldr1 (<>) es) (pure $ Right a)
+    FatalError es -> pure $ Left es
+    GenError es -> pure $ Left es
+    Result a -> pure $ Right a
 
--- Pass on the error messages of both kinds of Errors in the Gen (not the GenT) monad
-catchGen :: GenT GE a -> Gen (Either (NE.NonEmpty String) a)
+-- | Pass on the error messages of both kinds of Errors in the Gen (not the GenT) monad
+catchGen :: GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a)
 catchGen g = genFromGenT (catchGenT g)
 
 -- | Return the first successfull result from a list of computations, if they all fail
 --   return a list of the error messages from each one.
-firstGenT :: forall m a. MonadGenError m => [GenT GE a] -> GenT m (Either [NE.NonEmpty String] a)
+firstGenT ::
+  forall m a. MonadGenError m => [GenT GE a] -> GenT m (Either [(NonEmpty (NonEmpty String))] a)
 firstGenT gs = loop gs []
   where
-    loop :: [GenT GE a] -> [NE.NonEmpty String] -> GenT m (Either [NE.NonEmpty String] a)
+    loop ::
+      [GenT GE a] -> [NonEmpty (NonEmpty String)] -> GenT m (Either [NonEmpty (NonEmpty String)] a)
     loop [] ys = pure (Left (reverse ys))
     loop (x : xs) ys = do
       this <- catchGenT x
@@ -314,15 +376,16 @@ firstGenT gs = loop gs []
 liftGen :: forall x. (forall m. MonadGenError m => GenT m x) -> GenT GE x
 liftGen x = x
 
--- Drop a (GenT GE) computation into a (GenT m) computation. Some error information
--- is lost, as the two components of FatalError and GenError are folded into one component.
+-- Drop a (GenT GE) computation into a (GenT m) computation.
+-- Depending on the monad 'm' Some error information might be lost as
+-- the monad m might fold FatalError's and GenError's together.
 dropGen :: MonadGenError m => GenT GE a -> GenT m a
 dropGen y = do
   r <- inspect y
   case r of
-    FatalError es e -> fatalError (foldr1 (<>) es <> e)
-    GenError es e -> genError (foldr1 (<>) es <> e)
-    Result es a -> explain (foldr1 (<>) es) (pure a)
+    FatalError es -> fatalErrors es
+    GenError es -> genErrors es
+    Result a -> pure a
 
 -- | Run one of the actions with frequency proportional to the count. If it fails, run the other.
 frequency2 :: forall m a. MonadGenError m => (Int, GenT GE a) -> (Int, GenT GE a) -> GenT m a
@@ -339,23 +402,14 @@ frequency2 (n, g1) (m, g2)
 
 -- ======================================
 
--- | Temporarily extend the stack while executing 'm', and revert to the old stack if successful
-push :: forall m a. MonadGenError m => [String] -> GenT GE a -> GenT m a
-push [] m = dropGen m
-push (x : xs) m =
-  case explain (x NE.:| xs) m of
-    GenT f -> (GenT g)
-      where
-        g :: GenMode -> Gen (m a)
-        g mode = do
-          result <- f mode
-          case result of
-            Result (_ : ys) a -> pure $ runGE (Result ys a)
-            other -> pure $ runGE other
+-- | like explain for GenT, but uses [String] rather than (NonEmpty String)
+--   if the list is null, it becomes the identity
+push :: forall m a. MonadGenError m => [String] -> m a -> m a
+push [] m = m
+push (x : xs) m = explain (x :| xs) m
 
+-- | like explain for GE, but uses [String] rather than (NonEmpty String)
+--   if the list is null, it becomes the identity
 pushGE :: forall a. [String] -> GE a -> GE a
 pushGE [] x = x
-pushGE (x : xs) m = do
-  case explain (x NE.:| xs) m of
-    Result (_ : ys) a -> Result ys a
-    other -> other
+pushGE (x : xs) m = explain (x :| xs) m
diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs
index 0f78cc77c0a..00315605052 100644
--- a/libs/constrained-generators/src/Constrained/Properties.hs
+++ b/libs/constrained-generators/src/Constrained/Properties.hs
@@ -51,7 +51,7 @@ prop_sound ::
 prop_sound spec =
   QC.forAllBlind (strictGen $ genFromSpecT spec) $ \ma ->
     case ma of
-      Result _ a ->
+      Result a ->
         QC.cover 80 True "successful" $
           QC.counterexample (show a) $
             monitorSpec spec a $
diff --git a/libs/constrained-generators/src/Constrained/SumList.hs b/libs/constrained-generators/src/Constrained/SumList.hs
index ec7b1d64b6c..a0f0cae7b5f 100644
--- a/libs/constrained-generators/src/Constrained/SumList.hs
+++ b/libs/constrained-generators/src/Constrained/SumList.hs
@@ -25,22 +25,23 @@ instance Show t => Show (Solution t) where
 --   The one wrinkle is if everything is No, then in that case return an arbitrary one of the No's.
 --   This can be done in linear time in the length of the list. Call that length n.
 --   Check for all No. This takes time proportional to n. If it is true return one of them.
---   If it is not true. Concat all the Yes, and skip all the No.
+--   If it is not all No, then concat all the Yes, and skip all the No.
 --   We find the first No (if it exist), and all the Yes by partitioning the list
 --   This is similar in spirit to Constrained.GenT.catGEs, but doesn't require a
 --   a Monad to escape on the first No.
-concatSolution :: Show t => t -> String -> t -> Int -> [Solution t] -> Solution t
-concatSolution smallest pName total count sols =
+concatSolution :: Show t => t -> t -> String -> t -> Int -> [Solution t] -> Solution t
+concatSolution smallest largest pName total count sols =
   case partitionEithers (map (\case Yes x -> Left x; No x -> Right x) sols) of
     ([], n : _) -> No n -- All No, arbitrarily return the first.
     (y : ys, _) -> Yes $ sconcat (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
+        [ "\nThe sample in pickAll was empty"
+        , "  smallest = " ++ show smallest
+        , "  largest = " ++ show largest
+        , "  pred = " ++ pName
+        , "  total = " ++ show total
+        , "  count = " ++ show count
         ]
 
 newtype Cost = Cost Int deriving (Eq, Show, Num, Ord)
@@ -55,13 +56,13 @@ firstYesG nullSolution f xs c = go xs c
       ans <- f x (cost + 1)
       case ans of
         (cost1, No _) -> go more cost1
-        (cost2, Yes y) -> pure (cost2, Yes y)
-        _ -> pure ans
+        (_, Yes _) -> pure ans
 
 noChoices :: Show t => Cost -> String -> t -> t -> t -> Int -> [(t, t)] -> Solution t
 noChoices cost p smallest largest total count samp =
   No
-    [ "No legal choice can be found, where"
+    [ "\nNo legal choice can be found, where for each sample (x,y)"
+    , "x+y = total && predicate x && predicate y"
     , "  predicate = " ++ p
     , "  smallest = " ++ show smallest
     , "  largest = " ++ show largest
@@ -74,7 +75,6 @@ noChoices cost p smallest largest total count samp =
 
 -- =====================================================
 
-
 -- | 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),
@@ -83,7 +83,6 @@ splitsOf :: Integral b => b -> [(b, b)]
 splitsOf count = [(i, j) | i <- [1 .. div count 2], let j = count - i]
 {-# SPECIALIZE splitsOf :: Int -> [(Int, Int)] #-}
 
-
 -- | Given a Path, find a representative solution, 'ans', for that path, such that
 --   1) (length ans) == 'count',
 --   2) (sum ans) == 'total'
@@ -131,7 +130,7 @@ pickAll smallest largest (pName, _) total count cost
       pure $
         ( cost
         , No
-            [ "pickAll exceeds cost limit " ++ show cost
+            [ "\nPickAll exceeds cost limit " ++ show cost
             , "  predicate = " ++ pName
             , "  smallest = " ++ show smallest
             , "  largest = " ++ show largest
@@ -148,7 +147,11 @@ pickAll smallest largest (pName, _) total count cost
       pure $
         ( cost
         , No
-            [ "The feasible range to pickAll [" ++ show smallest ++ " .. " ++ show (div total 2) ++ "] was empty"
+            [ "\nThe feasible range to pickAll ["
+                ++ show smallest
+                ++ " .. "
+                ++ show (div total 2)
+                ++ "] was empty"
             , "  predicate = " ++ pName
             , "  smallest = " ++ show smallest
             , "  largest = " ++ show largest
@@ -184,15 +187,14 @@ pickAll smallest largest (pName, p) total count cost = do
           else pure (splitsOf count)
 
   firstYesG
-    (No ["No split has a solution", "cost = " ++ show cost])
+    (No ["\nNo split has a solution", "cost = " ++ show cost])
     (doSplit smallest largest (pName, p) total choices)
     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
+--  <$> mapM  (doSplit smallest largest total (pName, p) choices (pickAll (depth +1) smallest)) splits
 
 -- {-# SPECIALIZE pickAll::Int -> (String, Int -> Bool) -> Int -> Int -> Cost -> Gen (Cost, Solution Int) #-}
 
@@ -228,9 +230,10 @@ doSplit smallest largest (pName, p) total sample (i, j) c = go sample c
           pure $
             ( cost
             , No
-                [ "The sample passed to doSplit [" ++ show smallest ++ " .. " ++ show (div total 2) ++ "] was empty"
+                [ "\nThe sample passed to doSplit [" ++ show smallest ++ " .. " ++ show (div total 2) ++ "] was empty"
                 , "  predicate = " ++ pName
                 , "  smallest = " ++ show smallest
+                , "  largest = " ++ show largest
                 , "  total " ++ show total
                 , "  count = " ++ show (i + j)
                 , "  split of count = " ++ show (i, j)
@@ -240,20 +243,20 @@ doSplit smallest largest (pName, p) total sample (i, j) c = go sample c
           pure $
             ( cost
             , No
-                [ "All choices in (genSizedList " ++ show (i + j) ++ " 'p' " ++ show total ++ ") have failed."
+                [ "\nAll choices in (genSizedList " ++ show (i + j) ++ " 'p' " ++ show total ++ ") have failed."
                 , "Here is 1 example failure."
                 , "  smallest = " ++ show smallest
+                , "  largest = " ++ show largest
                 , "  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))
+                , "Predicate 'p' = " ++ pName
+                , "A small prefix of the sample, elements (x,y) where x+y = " ++ show total
+                , unlines (map (("  " ++) . show) (take 10 sample))
                 ]
             )
-
 {-# INLINE doSplit #-}
 
 -- | If the sample is small enough, then enumerate all of it, otherwise take a fair sample.
@@ -266,7 +269,6 @@ smallSample smallest largest total bound size
       shuffle [(x, total - x) | x <- choices]
 {-# INLINE smallSample #-}
 
-
 -- | 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)