Filtering list by minimum length fails when used in a property

[kerryb]

Firstly, I'm new to both property-based testing and this library, so apologies if this is user error.

I'm trying to write a property for something that's only applicable to lists with at least two elements, but I can't seem to generate values for the test. Here's a reduced example:

defmodule MyAppTest do
  use ExUnit.Case
  use PropCheck

  property "for a list with at least two elements, the tail is never empty", [:verbose] do
    forall [_ | tail] <- such_that(l <- non_empty(list(term())), when: length(l) > 1) do
      Enum.any?(tail)
    end
  end
end

When I run it, I get a "can't generate" error:

my_app$ mix test

Error: Couldn't produce an instance that satisfies all strict constraints after 50 tries.


  1) property for a list with at least two elements, the tail is never empty (MyAppTest)
     test/my_app_test.exs:5
     Property Elixir.MyAppTest.property for a list with at least two elements, the tail is never empty() failed with an error: {:error, :cant_generate}
     code: nil
     stacktrace:
       (propcheck) lib/properties.ex:185: PropCheck.Properties.handle_check_results/4
       test/my_app_test.exs:5: (test)

However, when I paste the same code into iex, it seems to work:

iex(1)> use PropCheck
PropCheck.TargetedPBT
iex(2)> produce(such_that(l <- non_empty(list(term())), when: length(l) > 1))
{:ok,
 [
   <<58, 117, 253, 188, 1::size(5)>>,
   [-2, {7}, 0, <<190, 21::size(6)>>, 11.336541195778157, []],
   -12,
   {{}, -7.661601316761714, :"", []}
 ]}

This is with propcheck 1.2.0, proper 1.3.0, elixir 1.9.4 and erlang 22.1.0, running on macOS 10.15.1.

[evnu]

For such cases, I usually build a generator that creates the first two elements and appends a possibly empty list of elements. This has the advantage that it always succeeds, so the constraint will never fail. Example:

def at_least_two_integers do
  let [first <- integer(), second <- integer(), many <- list(integer())], do:
    [first, second | many]
end

This can then be used in forall:

property "all integers" do
  forall ints <- at_least_two_integers() do
    Enum.all?(ints, &is_integer/1)
  end
end

[evnu]

But I also wonder why such_that seems to generate only small instances of lists in your example. Maybe PropEr's generation strategy does not work well with such_that. @alfert do you have more insight into this?

[kerryb]

Thank you @evnu! I'd tried a similar approach, but the thing I was missing was let.

[alfert]

do you have more insight into this?

No, sorry, not yet. But I can confirm, that it behaves exactly the same for me. Very annoying, at least, if not a wrong implementation, some how.

[x4lldux]

It behaves that way, because it tries to generate instances of lists of size from 0 to 1 (default value of :start_size), until the constraint of suchthat is satisfied, which in this case will never happen. You would need to set :start_size to 2.

[kerryb]

Thanks @x4lldux – good explanation.

[alfert]

You would need to set :start_size to 2.

Indeed, this solves this puzzle. We need to document that behaviour. I was totally not aware of this.

[x4lldux]

@alfert it kinda already is. Might be clearer, though.
From docs of such_that/2 macro:

If this is the case, it would be more appropriate to generate valid instances
of the specialized type using the let macro. Also make sure that even
small instances can satisfy the constraint, since PropEr will only try
small instances at the start of testing. If this is not possible, you can
instruct PropEr to start at a larger size, by supplying a suitable value
for the :start_size option (see the "Options" section).