Sema: Opening overloads at the outer decision level, part 1 #82928
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.
Today, we open the type of an overload after we make the decision to bind it. The opening generates new type variables and constraints from the overload's generic signature. This results in exponential space usage in the solver arena when exploring a large search space, because we also form other structures such as function types, substitution maps, etc that involve these new type variables, but we never re-use those type variables or the structures built up from them after we backtrack. (We also don't incrementally roll back the solver arena when we backtrack, because that would require trail-recording changes to all the folding sets in the AST, which would probably not be worth the overhead.)
Instead, we're going to open the overload type when forming the disjunction, at scope N; this will generate new type variables and constraints without actually introducing them into the constraint system, and also build the opened type. The opened type, together with the type variables and constraints, will be stored in a PreparedOverloadChoice. When we attempt the disjunction, we will create scope N+1, and then introduce the prepared type variables and constraints.
This increases overhead in the case that some choices in a disjunction are never explored, because then we build the opened type and never use it. But it will pay off -- exponentially -- for expressions involving operators and other global overloads that are looked up at the outermost decision level, but are then repeatedly bound with different other combinations as we search.
This also won't help with member overloads as much, like foo.bar.baz, because the qualified lookups happen in nested decision levels, so we may still re-generate new opened types and type variables.
Preserving the "identity" of the type variables and constraints associated with an overload choice while we explore different parts of the search space should also help us implement non-chronological backtracking.