False positive `ParadoxicalCondition` when using `in_array()`

[corphi]

When given the snippet

function contains(array $list1, array $list2, mixed $element): void
{
    if (in_array($element, $list1, true)) {
    } elseif (in_array($element, $list2, true)) {
    }
}

the second condition is mistaken to be identical to the first condition.

See https://psalm.dev/r/e148c5660c

This has been introduced in Psalm 4.9.3.

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/e148c5660c

<?php

function contains(array $list1, array $list2, mixed $element): void
{
    if (in_array($element, $list1, true)) {
    } elseif (in_array($element, $list2, true)) {
    }
}

Psalm output (using commit 2e7763c):

ERROR: ParadoxicalCondition - 6:15 - Condition ($element is in-array-mixed) contradicts a previously-established condition ($element is not in-array-mixed)

[weirdan]

Also reported by @orklah here: #6233 (comment)

[supersmile2009]

I checked why it happens. Here's a quick summary:

1. Assertion is extracted as in-array-X.
2. Inside of if clause it's treated as is.
3. For use outside of if clause (which includes elseif too) it is negated and becomes !in-array-X.

Both of those assertions are correctly reconciled by SimpleAssertionReconciler (narrows down the type to array value type) and NegatedAssertionReconciler(keeps type as is, since !in-array-X assertion is inconclusive - variable can still be pretty much anything).
However IfElseAnalyzer as well as the analyzers under Psalm\Internal\Analyzer\Statements\Block\IfElse namespace check for paradoxical conditions using the raw (not reconciled) assertions.

One naive solution that I first thought of - just don't negate in-array assertion (return no clauses), since such assertion is inconclusive. However negated assertion is still useful in a few cases:

1. post-if scope after negated in_array

function assertInArray($x, $y) {
    if (!in_array($x, $y, true)) {
        // clause is negated - resulting in `!in-array-T`
        throw new Exception();
    }
    // Negated clause is negated again, turning it into a much more useful `in-array-T`
    return $x;
}

So if we don't return the first negated clause, there won't be the 2nd one.
2. Detecting nonsensical assertions, where there's no type intersection between needle and haystack, e. g. asserting integer variable is not in array of strings.

So I'm not sure how to better approach it. Psalm\Internal\Analyzer\AlgebraAnalyzer::checkForParadox() should probably make an exception for some of the clauses. But making it aware of in-array assertions specifically is probably not the best idea. I can see Psalm\Internal\Clause has a bunch of undocumented boolean properties ($wedge, $generated etc.). And checkForParadox() does make some exceptions and doesn't report a paradox based on them. So I was wondering if any of these properties could be used. However they aren't documented, so I decided to ask first if anyone knows what they are supposed to mean before trying to reverse-engineer the logic behind them.

[orklah]

I don't know the code here very well, two things come to my mind:

• In AssertionFinder::processFunctionCall, you know if you're inside a negation thanks to $negate. Maybe that could be used to detect cases when we do want to keep the negated assertion
• In assertions, there is a system where you can add =, ~ for special meaning. Here's the explanation: SmallerOrEqual includes null #5772 (comment). We could use that to make Psalm understand some assertions are not made to be negated I think

[weirdan]

I decided to ask first if anyone knows what they are supposed to mean before trying to reverse-engineer the logic behind them.

I don't know the code here very well

We're all basically reverse-engineering here.

since such assertion is inconclusive

Negated in-array can be conclusive, when used on enumerated types. E.g. when you have a bool that is not in array of false it's quite obviously true. Same for "a"|"b" !in-array of "b", etc. 4.9.3 is aware of that, and it would be regrettable to lose that.