Fix gadt lhs union #10676
Fix gadt lhs union #10676
Conversation
|
@smarter This is supposed to fix #10102. I think Still, both |
| @@ -434,15 +434,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling | |||
| def widenOK = | |||
| (tp2.widenSingletons eq tp2) | |||
| && (tp1.widenSingletons ne tp1) | |||
| && recur(tp1.widenSingletons, tp2) | |||
| && inFrozenGadt { recur(tp1.widenSingletons, tp2) } | |||
There was a problem hiding this comment.
I think this pattern (inFrozenGadt(recur)) should have its own method (inFrozenGadtRecur ?) which clearly documents how it differs from recur (the doc of recur says "recur should also not be used to compare approximated versions of the original types", but here we're intentionally violating that, which requires freezing the gadt bounds)
There was a problem hiding this comment.
I think it was already violated before, since here we are recursing on approximations of the type. I'm not sure if there's anything special about inFrozenGadt here, rather, the docs of recur already suggest that it shouldn't be used here. I think the correct solution would be to add a comment to each of these calls explaining why they violate expectations of recur, but I don't know what to put in that comment.
There was a problem hiding this comment.
Yes, it was violated and thus broken before, but my understanding is that this violation is not a soundness issue as long as we freeze the gadt bounds, it just leads to missing solutions, but this is something we do intentionally in some situations.
There was a problem hiding this comment.
So do you want me to add add a comment to all of these callsites that we intentionally call recur on an approximated type, as it doesn't in this specific case lead to unsoundness? I don't think this merits a new definition, not yet anyway seeing as it's isolated to a single match branch.
There was a problem hiding this comment.
So do you want me to add add a comment to all of these callsites that we intentionally call recur on an approximated type, as it doesn't in this specific case lead to unsoundness?
Are there other callsites than the three for which you wrapped with inFrozenGadt? If there are others, shouldn't they also be wrapped with inFrozenGadt?
There was a problem hiding this comment.
There are no other callsites that call .widenSingletons or .join, I checked that before opening the PR, should've mentioned it.
EDIT: because I guess you don't mean "are there any other callsites in TypeComparer which call recur w/ an approx'd type".
There was a problem hiding this comment.
EDIT: because I guess you don't mean "are there any other callsites in TypeComparer which call recur w/ an approx'd type".
That is what I meant yes.
These approximations shouldn't be used to derive GADTs constraints, just as the .widenSingleton approx shouldn't.
abgruszecki
force-pushed
the
fix-gadt-lhs-union
branch
from
3ce6938 to
cd2a20a
Compare
|
@odersky are you still going to take a look at this, or should we just merge it? |
Fixes #10102.