Invalid ParadoxicalCondition raised with nested conditions in if statement

[driehle]

The following code raises two ParadoxicalCondition errors:

$isImmutable = substr($typeOfField, -9) === 'immutable';

if (
    ($isImmutable && $value instanceof DateTimeImmutable)
    || (! $isImmutable && $value instanceof DateTime)
) {
    return $value;
} elseif ($isImmutable && $value instanceof DateTime) {
    return DateTimeImmutable::createFromMutable($value);
} elseif (! $isImmutable && $value instanceof DateTimeImmutable) {
    return DateTime::createFromImmutable($value);
}

ERROR: ParadoxicalCondition - src/DoctrineObject.php:620:23 - Condition (($value is DateTime) && ($isImmutable)) contradicts a previously-established condition ($value is not DateTime) (see https://psalm.dev/089)
                } if ($isImmutable && $value instanceof DateTime) {


ERROR: ParadoxicalCondition - src/DoctrineObject.php:622:27 - Condition (($value is DateTimeImmutable) && (!$isImmutable)) contradicts a previously-established condition ($value is not DateTimeImmutable) (see https://psalm.dev/089)
                } elseif ((! $isImmutable) && $value instanceof DateTimeImmutable) {

Rewriting the first if condition in two statements makes the error disappear:

$isImmutable = substr($typeOfField, -9) === 'immutable';

if ($isImmutable && $value instanceof DateTimeImmutable) {
    return $value;
} elseif (! $isImmutable && $value instanceof DateTime) {
    return $value;
} elseif ($isImmutable && $value instanceof DateTime) {
    return DateTimeImmutable::createFromMutable($value);
} elseif (! $isImmutable && $value instanceof DateTimeImmutable) {
    return DateTime::createFromImmutable($value);
}

Code example: https://psalm.dev/r/d26bab675e

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/d26bab675e

<?php declare(strict_types=1);

class DoctrineObject
{
    /**
     * Handle various type conversions that should be supported natively by Doctrine (like DateTime)
     * See Documentation of Doctrine Mapping Types for defaults
     *
     * @link http://docs.doctrine-project.org/projects/doctrine-orm/en/latest/reference/basic-mapping.html#doctrine-mapping-types
     *
     * @param  mixed  $value
     * @param  string $typeOfField
     * @return mixed|null
     */
    protected function handleTypeConversions($value, $typeOfField)
    {
        $isImmutable = substr($typeOfField, -9) === 'immutable';

        if (
            ($isImmutable && $value instanceof \DateTimeImmutable)
            || (! $isImmutable && $value instanceof \DateTime)
        ) {
            return $value;
        } elseif ($isImmutable && $value instanceof \DateTime) {
            return DateTimeImmutable::createFromMutable($value);
        } elseif (! $isImmutable && $value instanceof \DateTimeImmutable) {
            return DateTime::createFromImmutable($value);
        }
        
        return null;
    }
}

Psalm output (using commit 0dc46c8):

ERROR: ParadoxicalCondition - 24:19 - Condition (($value is DateTime) && ($isImmutable)) contradicts a previously-established condition ($value is not DateTime)

INFO: MixedArgument - 25:57 - Argument 1 of DateTimeImmutable::createFromMutable cannot be mixed, expecting DateTime

ERROR: ParadoxicalCondition - 26:19 - Condition (($value is DateTimeImmutable) && (!$isImmutable)) contradicts a previously-established condition ($value is not DateTimeImmutable)

INFO: MixedArgument - 27:50 - Argument 1 of DateTime::createFromImmutable cannot be mixed, expecting DateTimeImmutable

[driehle]

@greg0ire has further simplified down the issue to https://psalm.dev/r/53f79d44aa.

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/53f79d44aa

<?php declare(strict_types=1);

/**
 * @param  mixed  $value
 * @return mixed|null
 */
function handleTypeConversions($value, bool $isImmutable): void
{
    if (
        ($isImmutable && $value instanceof \DateTimeImmutable)
        || (! $isImmutable && $value instanceof \DateTime)
    ) {
        // …
    } elseif ($isImmutable && $value instanceof \DateTime) {
        // …
    }
}

Psalm output (using commit 0dc46c8):

ERROR: ParadoxicalCondition - 14:15 - Condition (($value is DateTime) && ($isImmutable)) contradicts a previously-established condition ($value is not DateTime)

[orklah]

Reduced even more: https://psalm.dev/r/e79c2894ec

Must be a flaw in boolean module of Psalm. Which I believe is located in FormulaGenerator::getFormula. It's 400 lines of recursive boolean operations. It's gonna be tricky

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/e79c2894ec

<?php


function foo(bool $a, bool $b, bool $c): void
{
    if (($a && $b) || (! $a && $c)) {
        // …
    } elseif ($c) {
        // …
    }
}

Psalm output (using commit 0dc46c8):

ERROR: TypeDoesNotContainType - 8:15 - Operand of type false is always false

[muglug]

OK so this is tricky.

($a && $b) || (!$a && $c)

is expanded by Psalm to the conjunctive normal form

($a || $c) && (!$a || $b) && ($b || $c)

This equivalent (to Psalm) version demonstrates the same bug.

But when you enter that CNF into Wolfram Alpha it tells you the last term is unnecessary.

If you remove the unnecessary term the bug disappears.

The buggy method is Algebra::combineOredClauses, but I don't know how to fix it — combineOredClauses is a pretty simple method that just applies the standard distributed method for converting DNF to CNF. Then it looks like Algebra::negateFormula has incorrect behaviour when passed a formula with unnecessary terms, but I don't think that is a bug — negateFormula expects an optimal CNF.

I don't, honestly, remember how to obviously get the DNF to CNF conversion correct (missing the unnecessary term) on paper — once that was correct, fixing the combineOredClauses method wouldn't be too difficult. Either way the solution would probably slow down combineOredClauses.

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/76864ff3a5

<?php


function foo(bool $a, bool $b, bool $c): void
{
    if (($a || $c) && ($b || !$a) && ($b || $c)) {
        /** @psalm-trace $a */;
        /** @psalm-trace $b */;
        /** @psalm-trace $c */;
    } else {
        /** @psalm-trace $a */;
        /** @psalm-trace $b */;
        /** @psalm-trace $c */;
    }

}

Psalm output (using commit f7a6336):

INFO: Trace - 7:31 - $a: bool

INFO: Trace - 8:31 - $b: bool

INFO: Trace - 9:31 - $c: bool

INFO: Trace - 11:31 - $a: bool

INFO: Trace - 12:31 - $b: false

INFO: Trace - 13:31 - $c: false

https://psalm.dev/r/bc5487153d

<?php


function foo(bool $a, bool $b, bool $c): void
{
    if (($a || $c) && ($b || !$a)) {
        /** @psalm-trace $a */;
        /** @psalm-trace $b */;
        /** @psalm-trace $c */;
    } else {
        /** @psalm-trace $a */;
        /** @psalm-trace $b */;
        /** @psalm-trace $c */;
    }

}

Psalm output (using commit f7a6336):

INFO: Trace - 7:31 - $a: bool

INFO: Trace - 8:31 - $b: bool

INFO: Trace - 9:31 - $c: bool

INFO: Trace - 11:31 - $a: bool

INFO: Trace - 12:31 - $b: bool

INFO: Trace - 13:31 - $c: bool

[muglug]

Another example:

These two are functionally similar but give different output: https://psalm.dev/r/8f6b691a68

[psalm-github-bot]

I found these snippets:

https://psalm.dev/r/8f6b691a68

<?php

function foo(bool $a, bool $b, bool $c): void {
    if ((!$a && !$b) || ($a && $b) || ($a && $c)) {
        throw new \Exception();
    }

    if ($a) {}
}


function bar(bool $a, bool $b, bool $c): void {
    if ((!$a || $b || $c) && ($a || !$b)) {
        throw new \Exception();
    }

    if ($a) {}
}

Psalm output (using commit c885dbc):

ERROR: TypeDoesNotContainType - 8:9 - Operand of type false is always false

ERROR: TypeDoesNotContainType - 8:9 - Type false for $a is always !falsy

[muglug]

The solution is for me to add a rule to reduce the specific pattern

(A || <set of orred terms X>)
    && (!A || <set of orred terms Y>)
    && (<set of orred terms X> || <set of orred terms Y>)

to

(A || <set of orred terms X>)
    && (!A || <set of orred terms Y>)

i.e. when we have two clauses that negate a term within one another and another clause that's just the two uncontradicted terms together that clause is redundant. Should be a reasonably simple rule to add.

[orklah]

This is fixed on Psalm 5! Thanks Matt!