Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

James Coleman <jtc331(at)gmail(dot)com> writes:
> [ saop_is_not_null-v3.patch ]

There's still a logical problem here, which is that in order to
prove that the ScalarArrayOpExpr yields NULL when its LHS does,
you also have to prove that the RHS is not an empty array.
Otherwise you're up against the fact that the OR of zero boolean
expressions is false not null:

regression=# select null::int = any(array[]::int[]);
?column?
----------
f
(1 row)

While this is doable when the RHS is an array constant or ArrayExpr, I'm
afraid it's likely to be a bit tedious. (Hm, actually predicate_classify
already has logic to extract the number of elements in these cases ...
I wonder if there's any use in trying to share code?)

Minor stylistic quibble: I don't like where you inserted the new code in
clause_is_strict_for, because it renders the comment a few lines above
that unrelatable to the code. I'd put it at the bottom, after the
is_funcclause stanza.

regards, tom lane