Realizability: extra tests and code fix from #5558 #5726
Merged
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
Blaisorblade
added
the
fasttrack
This tests that b3dd07c is not *too* liberal.
Such a "variable" can only have one value, so this is okay. This goes back to 9125f58.
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. Beware 3: this also depends on unstable members with singletons types being stable.
Stack consumption grew apparently.
Blaisorblade
force-pushed
the
realizability-stray-tests
branch
from
f0551ac to
0ee31f4
Compare
Blaisorblade
changed the title
Blaisorblade
requested review from
odersky
and removed request for
nicolasstucki
Blaisorblade
removed
exp:novice
fasttrack
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.
Add a test for realizability, and one to check that b3dd07c in #5568 isn't too liberal.
Also add a behavior improvement from #5558. Follow-up cleanups are in #5730, but I'd like to first get a review from others to ensure this is clear enough to people.