All predicate failures must report non-empty

[lehins]

Any predicate failure that reports a data structure, must report a non-empty version of it. This will add an extra level of type safety by preventing a possibility of reporting a failure with nothing in it. We already do this for some predicate failures that report a list of things and we have a helper failOnNonEmpty that reports a non-empty list. We need to do the same for all such predicate failures and for predicate failures that contain maps and sets.

This will require usage of some library that provides non-empty versions of Set and Map. If there are no suitable libraries we can use, then we shall create thin wrappers around data types from containers in cardano-data with smart constructors that serve only this purpose.

This will also require some helpers in sts:

failOnNonEmptySet :: Ord a => Set a -> (NonEmptySet a -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmptyMap :: Ord k => Map k a -> (NonEmptyMap k a -> PredicateFailure sts) -> Rule sts ctx ()

[f-f]

Duplicate of #4066

[lehins]

Duplicate of https://github.com/IntersectMBO/cardano-ledger/issues/4066

Not exactly. #4066 is about non-empty lists, while this ticket is about Sets and Maps.