Intersection based gadts #6398
Intersection based gadts #6398
Conversation
abgruszecki
force-pushed
the
intersection-based-gadts
branch
from
97ef5bc to
2845895
Compare
abgruszecki
force-pushed
the
intersection-based-gadts
branch
from
2845895 to
db38c33
Compare
abgruszecki
force-pushed
the
intersection-based-gadts
branch
from
0b2c003 to
58c1cf6
Compare
|
@odersky This one's ready to go! This PR is the implementation of the "intersection-inspired" way of inferring GADT constraints that we talked about previously. It should be easiest to review it commit-by-commit. |
odersky
left a comment
odersky
left a comment
There was a problem hiding this comment.
The only serious problem I saw was in subsumes. The rest should be easy fixes.
| case AndType(scrut1, scrut2) => | ||
| constrainPatternType(pat, scrut1) && constrainPatternType(pat, scrut2) | ||
| case scrut: RefinedOrRecType => | ||
| constrainPatternType(pat, stripRefinement(scrut)) |
There was a problem hiding this comment.
You don't need stripRefinement. Can just do
constrainPatternType(pat, scrut.parent)(in both places where it is used). That does not special-case the natural recursion of constrainPatternType and removes a method.
Or is there something I overlooked?
| private [this] var leftRoot: Type = _ | ||
|
|
||
| /** Are we forbidden from recording GADT constraints? */ | ||
| private[this] var frozenGadt = false |
There was a problem hiding this comment.
I wondered, can this somehow be combined with the GADTflexible mode? I guess this would mean that instead of setting the GADTflexible mode bit we create a context with a new type comparer where frozenGadt is true.
...
After looking further I see that frozenGadt and GADTflexible are not equivalent. either depends on GADTflexible but not frozenGadt. I assume that's intentional.
There was a problem hiding this comment.
I can see how GADTFlexible and frozenGadt can appear to have the same purpose, though I don't really think of them this way. For me, GADTFlexible mode fundamentally alters isSubType(tp, pt) to mean "what type constraints necessarily follow from tp <: pt?", whereas frozenGadt is simply a temporary flag that TypeComparer sets for itself, much like ApproxState is a set of temporary flags that help with recording constraints.
At one point, frozenGadt was a part of ApproxState. Would it help if I called it gadtApprox and added more information to the comment?
| isSubType(tycon1.prefix, tycon2.prefix) && { | ||
| // check both tycons to deal with the case when they are equal b/c of GADT constraint | ||
| val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass | ||
| isSubArgs(args1, args2, tp1, tparams, inferGadtBounds = tyconIsInjective) |
There was a problem hiding this comment.
Would it not be better if frozenGadt was set around isSubArgs instead of for each individual arg? Fewer state changes and simpler logic since no additional parameter needs to be passed to isSubArgs.
The only thing that changes is that frozenGadt then also affects compareCaptured, but I don't see why it should not do that.
There was a problem hiding this comment.
Hm, I agree that the code will be a bit simpler if we just set frozenGadt around isSubArgs.
I believe that frozenGadt already affects compareCaptured, since it calls isSubArg.
| val saved = constraint | ||
| try | ||
| c2.forallParams(p => | ||
| pre.forallParams(p => |
There was a problem hiding this comment.
This is now in contradiction to the doc comment. Also, I don't see how it could capture the intended meaning.
If both c1 and c2 constrain different new type parameters that are not in pre, then according to the old meaning neither subsumes the other. But according to the new meaning each subsumes the other. This is clearly wrong, at least if we use the usual meaning of subsumes.
This seems to be a critical problem that requires further thought to be addressed.
GADT constraints are now inferred with an intersection-inspired algorithm. Inferencing.constrainPatternType was moved to PatternTypeConstrainer to organize the code better.
These tests were meant to test inferring GADT constraints based on type members, which we backed out of. They are still useful to see if we don't do anything unsound when type members are present.
Fixed soundness problems with abstract types - see test.
When going into arguments of a HKT, we only infer GADT constraints if we are certain that tycon is injective.
Previously, if c2 had instantiated a variable, it would not be iterated over and would not be compared with c1.
abgruszecki
force-pushed
the
intersection-based-gadts
branch
from
58c1cf6 to
01096ff
Compare
abgruszecki
dismissed
odersky’s stale review
Dismissing after confirming no re-review is necessary.
3 participants
This PR replaces GADT constraint inference algorithm with an intersection-inspired version.