Multiple forall in a property result in unexpected behaviour

[evnu]

When multiple forall or similar properties are used within a property, only the result of the last forall is relevant to the test result:

  property "multiple forall" do
    forall n <- nat() do
      n < 0
    end

    forall n <- nat() do
      n >= 0
    end
  end

This might come as a surprise to unexpecting users. PropCheck should probably warn about this.

[alfert]

The behaviour is exactly how it is implemented :-) It is the simple situation where you have a function with two expressions in the body. Only the latter will be the result:

def foo()
   3
   5
end

Function foo will return only 5. A property is simply a function in that sense. The only difference I can think of is if the first forall throws an exception.

[fenollp]

Doesn’t Elixir warn that 3 is an unused value though? Surely there’s a way to emit this warning as well when using macros like forall?

[alfert]

@fenollp, I don't think so. Macros generate an AST and do not inject Elixir source code as Erlang macros would do. So, the first steps of source code analysis within the Elixir compiler are not activated for the generated AST fragment. This is my general experience of writing macros. We could do something like implement it by ourselves, but this becomes difficult quickly when you think of nested forall macros.

What we certainly can do is to add a little statement within the docs of the property to make clear that a property is simply a function with a body. The result of the body is evaluated by the property macros and there is no magic happening (regarding the expecting a single value, not the mechanics of properties and the like 😄)

[fenollp]

I think the warnings about unused constructed values are generated by the compiler app and they get silenced when generating AST with the annotation “generated: true”.
So I’m thinking we may have 2 options:

• disable that annotation somehow when unquoting this specific macro
• find a way to expand the macro such that it creates a value of which the usage doesn’t get silenced by the compiler

It is quite possible that none of these options is possible given today’s semantics of Elixir in which case I would strongly encourage opening an issue on the language repo directly, as this sounds like an important enough feature to require the semantics.