Take HKT injectivity into account when inferring constraints #6461
Conversation
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
If we do not insert TypeVars into the bounds every time, then the only time we need to remove them is when taking the full bounds of some type. Since that logic now resides in ConstraintHandling and replaces all TypeParamRefs internal to SmartGADTMap, we have no need to perform expensive type traversals. This removes the only reason for caching bounds. The addition of HK parameter variance adaptation was necessary to make tests/pos/i6014-gadt.scala pass.
gadtSyms/gadtContext became redundant, so they were removed. The logic in typedDefDef was adjusted to only create a fresh context when necessary.
The rationale for using a Skolem here is: we want to record that there is at least one value that is both of the pattern type and the scrutinee type. All symbols are now considered valid for adding GADT constraints - the rationale is that set of constrainable symbols should be either selected on a per-(sub)pattern basis, or be the same for all matches. Previously, symbols which were only appearing variantly in a scrutinee type could be considered constrainable anyway because of an outer pattern match.
Also rename the classes to better reflect their role, and document and reorder definitions to make more sense.
The added symbols can have inter-dependencies in their bounds.
constrainPatternType is specific to term patterns, whereas in match types there is a simple subtyping relationship between the pattern and the scrutinee. In the future, simply calling isSubType in GADTFlexible context would likely be sufficient.
abgruszecki
changed the title
|
Integrated into #6398. |
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.
Based on top of #5736.
Fixes #5658.
I'd happily like to note that this works unreasonably well, given the size of the change - we can even see through aliases with no extra effort whatsoever.