-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix #4031, v3: Check arguments of dependent methods for realizability #5559
Conversation
I had a TypeError crash in refchecks after screwing up a typeclass encoding in a particularly bad way. This commit reports an error instead.
Extracted from 7659c11.
A TermRef is stable if its underlying type is stable. Realizability should behave the same way. Part 1 of 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.
Also streamline logic significantly.
The first attempt required changing z1720.scala; but that became unnecessary after aligning isRealizable with isStable. A TermRef is stable if its underlying type is stable. Realizability should behave the same way.
After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.
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.
31a6f89
to
fed7128
Compare
The failure appears genuine, in the interaction between staging and dependent types. The error in #5557 suggests this already happens when rebasing #4036 directly and without most of my changes to realizability. @odersky can you take a look? The error is in a call to dependent method
|
FWIW, the problem seems to arise from widening
|
I had a long and hard look at this, but did not come up with ideas. I don't see a reason to reject the failing examples, they should pass. We need to arrive at a version of realizability and So what happens is this:
So it seems we need to work on
I believe the difference is where the replacement for the unrealizable type is subsequently used in the substitution. For #4031 is appears left of a |
Closing since #4031 is not a bug that can be fixed right now. |
Fix #4031. This PR builds off #5558 and otherwise rebases the core changes related to that in #4036 (which were mostly about using realizability, not changing it).
There's still a fishy part from #4031 to make
tests/pos/i4031.scala
work:When typechecking
coerce3
, sincep
is unstable, the return type cannot bep.L
; sosafeSubstParam
eliminates references top
. Currently that producesAny#L
; so we either produce something better, or we add some kludge so thatAny#L <: Any
. In both cases, per testi4031-anysel.scala
, the user must still be forbidden from writingAny#L
. There are two solutions here (from @odersky):derivedSelect(tp, pre = Any)
to giveAny
, so thatAny#L
givesAny
.Any
a supertype of all types, similarly toAnyKind
, but keepingAny
kind-monomorphic (I think?) thanks toisLambdaSub
.