Filter-rewriting for length filters

[reaganjlee]

Resolves part of #3795

in this case we'll want to apply the rewrite for efficiency, and apply the predicate as a filter in case the name len has been rebound in the enclosing scope

So we take the components of the lambda and re-write with them. However, how would we keep in mind the case that the len function has been rebound/redefined? Or do you mean falling back to rejection sampling in this case?

[Zac-HD]

how would we keep in mind the case that the len function has been rebound/redefined? Or do you mean falling back to rejection sampling in this case?

Yep, falling back to rejection sampling here. Note that in the case where len wasn't redefined this is pretty cheap, because we'll never actually reject anything - just fail to generate some examples which would have been allowed.

[Zac-HD]

I've pushed a couple of tweaks and some more tests, and I think it's almost ready to merge - there's more we can do to support other collection types, but I'd like to ship what we have soon and then return for a follow-up PR. (both because it's easier to make and review smaller PRs, and so users can get some benefits asap)

Remaining tasks:

• Work out why some of the new tests are failing, and fix them
• Make the release note a bit less specific - we don't want to commit to a particular API here, so something like "This patch implements filter-rewriting for length bounds on some collections strategies." (plus the thankyou!) would be plenty.

[reaganjlee]

Got it, will have this done tomorrow after my flight!

[Zac-HD]

OK, I started to leave a code review, but the chain of reasoning I ended up going down was very long and the diff was pretty short, so I pushed it instead. In brief:

• I worked out that the test was failing because we were asserting that we had a TextStrategy from the partial(min_len, ...) filter, but we actually had a FilteredStrategy wrapping a TextStrategy.
• That was due to a change I'd made, where I had ListStrategy.filter unconditionally apply the original filter as a predicate. But that's wrong in this case, because we know that our custom length filters can't have len() rebound!
• So I moved the computation into the 'calculate the bounds' logic, and we now respect the original semantics of ConstructivePredicate - that if .predicate is non-None you must apply that too - and set it non-None for lambdas
• Which revealed that my check for distinct predicates in merge_preds was oversensitive, so I fixed that too...
• and finally I wrote a test to check that we can in fact apply multiple partial(min/max_len, ...) filters in a row and have them all rewritten, which means that we do get efficient strategies for from_type(Annotated[str, Len(2, 4)]) 💪

Whew. Notes longer than the diff?

[reaganjlee]

This is great! Thanks for the finish + writeup 😃