Ensure erased vals pass CheckRealizable #16111
Conversation
natsukagami
requested review from
nicolasstucki
and removed request for
nicolasstucki
|
Tests are breaking because |
natsukagami
changed the title
|
I guess we need to treat |
|
The scala compiletime package is using
|
|
|
||
| trait B { type L <: Nothing } | ||
| def upcast_dep_parameter(erased a: B)(x: a.L) : Int = x | ||
| erased val q : B { type L >: Any } = compiletime.erasedValue |
There was a problem hiding this comment.
Why is no error emitted on this line? What happens if I try to use q's bounds directly on the line below, without passing it as an argument to any function?
I feel like realizability should be checked whenever we try to create an erased value.
There was a problem hiding this comment.
Realizability checks are always performed when bounds are used, so using q's bounds directly will CE even without this PR.
This PR only adds the checks at function calls (they were performed at definition before, but they are not sufficient per the example).
I had a chat with @odersky about whether checks should be done when we create erased values. We concluded that it's okay to leave it at that to maximize flexibility of erased values.
There was a problem hiding this comment.
Ah. Then everything looks good to me.
... instead of checking every instantiated instance of erasedValue[T]. I think this is the better solution, since erasedValue have uses outside of erasedDefinitions (i.e. in inlining) which has their own realizability checks as well. We don't have to be pessimistic in those cases. - Only check for realizability for erased parameters of result-dependent functions. Per talk with @odersky, it seems that it is enough to check for realizability of parameters of a dependent function in order to avoid unsoundness. Note that the following actions have already been checked for, with erased parameters: - Using them as a dependent path in casting / variable definitions - Using them as the input to an `inline match` The check previously performed on `val`/`def` definitions are also removed, so we are as liberal as possible, to avoid too much restriction. I think with this, we can also remove the special case for `compiletime.erasedValue`.
natsukagami
force-pushed
the
4060-check-realizability-of-erased
branch
from
28b055e to
49906dd
Compare
natsukagami
force-pushed
the
4060-check-realizability-of-erased
branch
from
49906dd to
e770df3
Compare
Fix #4060: Ensure erased vals pass CheckRealizable
Per @odersky's comment, we wish to add realizability checks to all erased vals.
erased#4060 and small change in i11896