Refine GADT casts on singletons #11987
Conversation
- keep the singleton type in the cast target - assert cast target stability if original was stable - fix isStable test for TypeParamRefs - double check if GADT logic is really needed before inserting a cast Fixes scala#11220 Fixes scala#11955
| case CompareResult.OKwithGADTUsed if pt.isValueType => | ||
| case CompareResult.OKwithGADTUsed | ||
| if pt.isValueType | ||
| && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) { |
There was a problem hiding this comment.
@abgruszecki Not sure this is the right criterion. We need a way to make sure that the tree type conforms to the expected type without taking GADT constraints into account.
There was a problem hiding this comment.
If that's the intention, then this check makes perfect sense.
There was a problem hiding this comment.
Mostly everything LGTM. I tried to remove the code for adding the Stable annotation here (#12015) and it seems like no test failed. Could it be that some test wasn't committed?
| case CompareResult.OKwithGADTUsed if pt.isValueType => | ||
| case CompareResult.OKwithGADTUsed | ||
| if pt.isValueType | ||
| && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) { |
There was a problem hiding this comment.
If that's the intention, then this check makes perfect sense.
| && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) { | ||
| (tree.tpe.widenExpr frozen_<:< pt) | ||
| // we overshot; a cast is not needed, after all. (this happens a lot. We should | ||
| // find out whether we can make GADTused more precise) |
There was a problem hiding this comment.
It seems strange that we'd overshoot often. Could it be that this line is a culprit? It should be debuggable reasonably easily, by printing type comparison traces for the subtype check with and without GADT constraints, right at this code line. I'll take a look.
There was a problem hiding this comment.
"this" gives me a 404 😸
There was a problem hiding this comment.
Ah, the branch was wrong, it's this link: https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L503
There was a problem hiding this comment.
Yes, that's a possible source since we do GADT reasoning before falling back to fourthTry. I tried to swap the order of the two clauses but that gives inference errors.
i11995.scala failed before I added the refinement to re-check whether a GADT cast was needed. I think it should be possible to come up with a test that exercises i11955 with a GADT cast. |
|
I think we should come up with a test like that, otherwise we risk regressing. |
OK, I leave that to you. |
|
OK, I pushed some changes but GH doesn't want to cooperate. I'll reopen the PR. |
Fixes #11220
Fixes #11955