Shared: Add a Universal Flow library and refactor TypeFlow to use it. #17863
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.
Universal flow is the dual of existential flow in the sense that universal quantification replaces existential quantification in the recursive step in the reachability calculation. The existing shared TypeFlow library uses universal flow in several instances to prove additional type bounds that are stricter than the given static type.
This PR extracts the core universal flow calculation from TypeFlow and puts it in a separate library, such that we can easily apply it to other use-cases beyond TypeFlow. In order to do this, I had to make some very minor tweaks to the TypeFlow predicates, so the calculated bounds are not exactly the same, but they're very close:
exactType
should be preserved tuple-for-tuple.typeFlow
now includesexactType
as additional bounds directly instead of accounting for these in the (prior)supportsType
predicate. This simplifies things and only makes a tiny difference since the exact bounds are filtered afterwards.hasUnionTypeFlow
shifts slightly to put the base case on nodes rather than both nodes and edges. Again this simplifies things and only makes a tiny difference in the end when superfluous bound disjuncts are pruned.Commit-by-commit review is encouraged - I've tried hard to break the refactoring down into easily reviewable parts.