Fix #4031, v2: Check arguments of dependent methods for realizability (WIP) #5557
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
We were forgetting to check the prefix in the uncached case.
This change also caches stability for the affected code path.
After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.
Extracted from 7659c11.
Add the rule T <: Any for any *-Type T. This was not include fully before. We
did have the rule that T <: Any, if Any is in the base types of T. However,
it could be that the base type wrt Any does not exist. Example:
Any#L <: Any
yielded false before, now yields true. This error manifested itself in i4031.scala.
With the new rule, we can drop again the special case in derivedSelect.
TODO: in the context of scala#4108, this seems questionable. Also, `Any#L` seems an
invalid type (even tho it is sound to consider it empty), and we'd probably not
want to accept it if the user writes it; here it is only OK because it's
introduced by avoidance. Or are user-written types checked elsewhere?
A TermRef is stable if its underlying type is stable. Realizability should behave the same way. This obviates the change in z1720.scala.
I had a TypeError crash in refchecks after screwing up a typeclass encoding in a particularly bad way. This commit reports an error instead.
I wrote this because I feared (incorrectly) exponential slowdowns in realizability checking for this code. But debugging suggests that the complexity of realizability checking is constant in the size of these expressions (even after I disable caching of `Stable`). Beware 1: these expressions almost smash the stack by sheer size. Beware 2: this fails with `-Yno-deep-subtypes`, but simply because the checking heuristics assumes people don't try to do this.
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.
WIP rebase of #4031, finally. Still running tests.