Improved the error messages when a Spec fails. (#4739)

The function explainSpec no longer drops explanations on TypeSpec
Added guardTypeSpec, which catches errors earlier, so there is less noise.
function symbols like subset_ and member_ print a elided version of their set
arguments when they are large literals. Improves readabilty as irrelevant
information no longer overwhelms the user.
Add the constructor ExplainSpec to Specification
Assert now has type Assert :: Term fn Bool -> Pred fn
Added checks that ExplainSpec is handled correctly in Base.hs

eras/byron/chain/executable-spec/byron-spec-chain.cabal

@@ -62,5 +62,5 @@ test-suite chain-rules-test
         tasty-hedgehog,
         tasty-hunit,
         byron-spec-chain,
-        byron-spec-ledger,
+        byron-spec-ledger >=1.0,
         small-steps:{small-steps, testlib} >=1.1

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs

@@ -1687,6 +1687,7 @@ instance CoercibleLike (CompactForm Coin) Word64 where
     , reify x' unCompactCoin (==. V x)
     ]
   coerceSpec TrueSpec = TrueSpec
+  coerceSpec (ExplainSpec es x) = ExplainSpec es (coerceSpec x)
 
   getCoerceSpec ::
     forall (fn :: [Type] -> Type -> Type).
@@ -1762,6 +1763,8 @@ toDelta_ ::
 toDelta_ = app toDeltaFn
 
 instance (Typeable fn, Member (CoinFn fn) fn) => Functions (CoinFn fn) fn where
+  propagateSpecFun fn ctx (ExplainSpec [] s) = propagateSpecFun fn ctx s
+  propagateSpecFun fn ctx (ExplainSpec es s) = ExplainSpec es $ propagateSpecFun fn ctx s
   propagateSpecFun _ _ TrueSpec = TrueSpec
   propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err
   propagateSpecFun fn (ListCtx pre HOLE suf) (SuspendedSpec x p) =

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs

@@ -49,7 +49,7 @@ import Cardano.Ledger.UMap (CompactForm (..))
 import qualified Cardano.Ledger.UMap as UMap
 import Cardano.Ledger.UTxO (UTxO (..))
 import Constrained hiding (Value)
-import Constrained.Base (Pred (..), hasSize, rangeSize)
+import Constrained.Base (Pred (..))
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Set (Set)

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Tests.hs

@@ -26,7 +26,6 @@ import Cardano.Ledger.Shelley.LedgerState (
  )
 import Cardano.Ledger.UTxO (UTxO (..))
 import Constrained hiding (Value)
-import Constrained.Base (hasSize, rangeSize)
 import Data.Kind (Type)
 import Data.Map (Map)
 import qualified Data.Set as Set

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs

@@ -32,7 +32,6 @@ import Cardano.Ledger.SafeHash ()
 import Cardano.Ledger.Shelley.LedgerState
 import Cardano.Ledger.UTxO (UTxO (..))
 import Constrained hiding (Value)
-import Constrained.Base (hasSize, rangeSize)
 import Data.Map (Map)
 import Test.Cardano.Ledger.Constrained.Conway ()
 import Test.Cardano.Ledger.Constrained.Conway.Instances

libs/constrained-generators/src/Constrained.hs

@@ -37,6 +37,7 @@ module Constrained (
   MapSpec (..),
   FoldSpec (..),
   simplifySpec,
+  addToErrorSpec,
   genFromSpecT,
   genFromSpec,
   genFromSpecWithSeed,
@@ -117,6 +118,8 @@ module Constrained (
   cNothing_,
   cJust_,
   null_,
+  rangeSize,
+  hasSize,
   injectFn,
   app,
   lit,