Defer boolean-decomposition narrowing to the application point - #6163
Merged
Conversation
SpecifiedTypes carries conditional-expression-holder recipes and deferred augments; filterBySpecifiedTypes() evaluates both against the applying scope - the application point of the narrowing - instead of the scope the composition ran on. The setters switch to clone so new slots can never be dropped by a copying setter. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7
BooleanAnd/BooleanOr compose recipes and deferred augments instead of running the holder math, the either-branch union recovery and the disjunction-truthy holder projection eagerly on the composition scope. The decided-operand arms return the raw narrowing - the sure-not entries stay symbolic and resolve where they are applied. Expectation updates match the deferred evaluation: empty() on a variable that is truthy whenever defined now proves the variable undefined in the empty() branch, and a template-typed subject is no longer re-wrapped inside its own bound (T of T of ...) by the branch-union recovery. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7
Both false positives - the property-narrowing leak and the in_array() set-narrowing leak past an intermediate if - are fixed by deferring the boolean-decomposition holder math to the application point. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7
…e truth The antecedent-swap fallback stands the inverted truthy narrowing in for "this side of the && is true", which is only sound when the narrowing is equivalent to the side's truth. isset() qualifies - it is exactly the offset's non-nullness. A call like non-strict in_array($x, $a) does not: its truthy narrowing (a non-empty $a) can hold while the call is false, and the derived holder unsoundly narrowed the other operand ($x to null) in a sibling branch where only $a !== [] was known. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7
The applying-scope certainty gate of the disjunction-truthy holder projection is pinned by a stored-boolean fixture with a Maybe-defined target - a projected sure type would wrongly upgrade its certainty. The per-branch certainty guards had no reachable divergent state: the branch scopes are filtered views of the very scope the narrowing is applied on, so their tracked certainty cannot drop below it. The bug-14908 rule tests require PHP 8.1 (enums) at runtime, not just for fixture linting. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The
applySpecifiedTypesarc from the resolve-type-rewrite branch (the symbolic alternative-form entries already landed earlier — this completes the deferral), plus two conditional-holder soundness fixes built on it:SpecifiedTypescarries conditional-expression-holder recipes and deferred augments;MutatingScope::filterBySpecifiedTypes()evaluates both against the applying scope — the application point of the narrowing — instead of the scope the composition ran on. Setters switch tocloneso a copying setter can never silently drop a slot.BooleanAndHandler/BooleanOrHandlercomposeConditionalExpressionHolderRecipes, aDisjunctionBranchUnionAugment(either-branch union recovery) and aDisjunctionHolderProjectionAugment(disjunction-truthy holder projection) instead of running that math eagerly; the branch scopes are thunks, so deep boolean chains no longer derive every level's opposite-polarity scope. The decided-operand arms return the raw narrowing — sure-not entries stay symbolic and resolve where applied. The four eager helper methods are gone. Locally this is a −2.6% self-analysis win (ABBA, n=6 per side).if— regression-tested against both of its symptoms (identical.alwaysFalseon the property,function.alreadyNarrowedTypeon thein_array()set check).isset()), not merely implied by it: non-strictin_array($x, $a)'s truthy narrowing (non-empty$a) can hold while the call is false, and the derived holder unsoundly pinned$xtonullin a sibling branch where only$a !== []was known.Expectation updates (each matching the rewrite branch, reviewed individually):
empty($foo)on a truthy-when-defined variable now proves$fooundefined in the branch (certainty No); a template-typed subject is no longer re-wrapped inside its own bound (T of T of ...); twoTypeSpecifierTestrows expect the application-point subtraction form forempty($array).Known downstream churn: Rector's
AssignArrayToStringRectorskip-fixtureskip_reassigned_as_string.php.incstarts failing — its$whereis conditionally assigned a truthy value, so insideif (empty($where))PHPStan now correctly proves it undefined (previously maybe-defined with the eagerarray{}), which flips Rector's skip-heuristic. Their fixture/heuristic needs adapting to the more precise inference.Everything else is churn-free: NodeScopeResolverTest 1696, full suite 17820,
make phpstan,make cs.Closes phpstan/phpstan#14908
Closes phpstan/phpstan#14966
🤖 Generated with Claude Code
https://claude.ai/code/session_01DaBZjgksga4c5s6Q9FniY7