Gadt unification #5611
Merged
Gadt unification #5611
Conversation
This file contains 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
This reverts commit 756cd0a.
Allow abstracting over what context is needed by ConstraintHandling.
odersky
requested changes
Dec 14, 2018
| if ((tycon2bounds.lo `eq` tycon2bounds.hi) && !tycon2bounds.isInstanceOf[MatchAlias]) | ||
| if (followSuperType) recur(tp1, tp2.superType) |
There was a problem hiding this comment.
It reverted commit fills a hole in the subtype checker. What tests failed before we reverted it? It would be good to find a root cause for the failure.
There was a problem hiding this comment.
TypeSafeLambda failed. Since this PR anyway leaves GADTs using HKTs unsound, I wanted to focus first on solving #5630, and then to come back to this problem.
There was a problem hiding this comment.
OK, agreed. Maybe make an issue so that it is not forgotten?
| case tv: TypeVar => tv | ||
| case inst => | ||
| gadts.println(i"instantiated: $sym -> $inst") | ||
| // this is wrong in general, but "correct" due to a subtype check in TypeComparer#narrowGadtBounds |
There was a problem hiding this comment.
Fixed by inlining the code from TypeComparer#narrowGADTBounds. Inlining it did not work previously, but whatever code was causing that must've changed along the way.
|
Overall this looks good. I have only minor comments. |
abgruszecki
commented
Dec 17, 2018
odersky
approved these changes
Dec 17, 2018
This was referenced Dec 23, 2018
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.
Cleaned up version of #5258.
Copying over relevant information:
This fixes all of the below:
For the time being, we mishandle injectivity and so we are unsound. See tests/run/gadt-injectivity-unsoundness.scala for a test showing a class cast exception. We will need to create an issue for this.
756cd0a was reverted because it was making the tests fail, and reverting it caused no test failures. I might bring it back later when working on injectivity.
At first glance, it might make sense to merge
GADTMapstate withTyperState. However, it's not necessary (since it's possible to just keep a fresh copy ofGADTMapas the "state") and it's not entirely obvious how to adapt already existing code. See #5258 (comment) for detailed reasoning. For the time being, I think it'd be best to leave the state where it is and refactor later if handling the GADT state becomes problematic.