IntersectMBO / IntersectMBO/cardano-ledger
`constrained-generators`: poor useability for interaction between `forAll` and `dependsOn`
- Dominant language
- Haskell
- Stars
- 295
- Forks
- 179
- Avg merge
- 4d 7h
- Merged PRs (30d)
- 29
Description
If you write the following code:
```haskell
listSetRelation :: Spec BaseFn ([Int], Set Int)
listSetRelation = constrained' $ \xs ys ->
[ forAll xs $ \ x ->
[ x `member_` ys
, 0 <. x
]
, ys `dependsOn` xs
]
```
The intention is to generate a list of positive numbers, and then put them all in the set. However, what happens instead is that we generate a list of numbers, and then fail generation if any of them happen to be non-positive:
```
$> quickCheck $ checkCoverage $ prop_sound listSetRelation
*** Failed! Insufficient coverage (after 100 tests):
8% successful
Only 8% successful, but expected 80%
```
However, you can rewrite the generator by splitting the `forAll`:
```haskell
listSetRelation' :: Spec BaseFn ([Int], Set Int)
listSetRelation' = constrained' $ \xs ys ->
[ forAll xs $ \ x -> 0 <. x
, ys `dependsOn` xs
, forAll xs $ \ x -> x `member_` ys
]
```
and `quickCheck` is happy as ever:
```
$> quickCheck $ checkCoverage $ prop_sound listSetRelation'
+++ OK, passed 100 tests (100% successful).
```
Now, if you understand how the system works this is something you can work around, but it would be nice for usability if we did the split automatically (it can be inferred from the `dependsOn`).
Contributor guide
Assessment
This issue has not been assessed yet.