Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

James Coleman <jtc331(at)gmail(dot)com> writes:
> I forgot to update in v8 so attaching v9.

So ... this is actively wrong.

This case shows that you can't ignore the empty-array possibility
for a ScalarArrayOpExpr with useOr = false, because
"SELECT null::int = all(array[]::int[])" yields TRUE:

contrib_regression=# select * from test_predtest($$
select x is not null, x = all(array(select i from generate_series(1,0) i))
from integers
$$);
WARNING: strong_implied_by result is incorrect
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f

This case shows that you can't ignore the distinction between null
and false results once you've descended through strict function(s):

contrib_regression=# select * from test_predtest($$
select x is not null, strictf(true, x = any(array(select i from generate_series(1,0) i)))
from integers
$$);
WARNING: strong_implied_by result is incorrect
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f

(In this usage, the strictf() function from the test_predtest.sql
will simply return the NOT of its second input; so it gives different
answers depending on whether the SAOP returned false or null.)

I think you could probably repair the second problem by adding
an additional argument to clause_is_strict_for() indicating whether
it has to prove the clause to be NULL or merely non-TRUE; when
recursing you'd always have to ask for the former.

The first problem could be resolved by insisting on being able to
prove the array non-empty when !useOr, but I'm not sure if it's
really worth the trouble, as opposed to just not trying to prove
anything for !useOr cases. I'm not sure that "x op ALL(ARRAY)"
occurs often enough in the wild to justify expending code on.

The other case where being able to prove the array nonempty might
be worth something is when you've recursed and hence need to be
able to prove the SAOP's result to be NULL not just not-TRUE.
Again though, I don't know how often that occurs in practice,
so even the combination of those two motivations might not be
worth having code to check the array argument.

It'd also be worth spending some brain cells on what happens
when the SAOP's array argument is null overall, which causes
its result to be null (not false). Maybe the logic goes
through without needing any explicit test for that case
(and indeed I couldn't break it in testing that), but it'd
likely be worth a comment.

I don't especially care for the proposed function name
"clause_proves_for_null_test". The only thing that brings to my
mind is the question "proves WHAT, exactly?" --- and as these
examples show, being crystal clear on what it proves is essential.

regards, tom lane