Tighten comparison of skolem types #599
Conversation
odersky
force-pushed
the
add/existential-skolemization
branch
from
5fe845e to
1bb6703
Compare
| var res = asSeenFrom(tp, pre, cls, m) | ||
| if (m != null && m.unstable) asSeenFrom(tp, SkolemType(pre), cls) else res | ||
| } | ||
|
|
||
| final def asSeenFrom(tp: Type, pre: Type, cls: Symbol, theMap: AsSeenFromMap): Type = { |
There was a problem hiding this comment.
This method and its parameters should be documented.
|
The PR is now complete. I'll try to improve the documentation parts. This whole PR is pretty-subtle because it covers an essential, and largely unresearched part of path dependent types. |
Skolem types are =:= only if they are reference-equal. Two skolem types with the same underlying type are not necessarily equal. Tests continue to run under this tightened definition.
A term ref is stable only if its prefix is also stable. At the same time, we drop stability requirements where they no longer make sense (e.g. in isLegalPrefix).
Be more aggressive doing this than with lookupRefined in that we compute the member of a projected name, instead of just analyzing the type structurally. Reason: (1) If we do not follow aliases, skolemization will lose information (2) Skolemization is applied rather late, less risk of cyclic references by computing members.
(1) Refinements of stable types are stable (2) TypeVars instantiated to stable types are stable.
Will use deskolemize later, when method result types are inferred.
SkolemTypes need to behave differently form RefinedThis types in TypeMap and TypeAccumulator. For skolem types these should follow through to the underlying type. For RefinedThis types, these need to do nothing, in order not to start an infinite recursion.
Skolem[T] != Skolem[T]
It's no longer needed in TypeComparer. We now deskolemize when locally inferring types of vals and defs.
Skolemize unstable prefixes in asSeenFrom provided - the prefix appears at least once in non-variant or contra-variant position - we are in phase typer. After typer, we have already established soundness, so there's no need to do skolemization again. We can simply do the (otherwise unsound) substitution from this-type to prefix.
We want to establish the invariant (optionally checked by assertNoSkolems) that symbols do not contain skolemized types as their info. This avoids unsoundness situations where a skolem gets exported as part if the result type of a method, so different instantiations look like their are the same instance.
neg/projections required certain types of the form C#T to be ill-formed. This is no longer done.
odersky
force-pushed
the
add/existential-skolemization
branch
from
e0d2567 to
081b6ad
Compare
|
Rebased to master |
| @@ -103,10 +103,10 @@ Standard-Section: "ASTs" TopLevelStat* | |||
| TERMREFpkg fullyQualified_NameRef | |||
| TERMREF possiblySigned_NameRef qual_Type | |||
| THIS clsRef_Type | |||
| SKOLEMtype refinedType_ASTRef | |||
| REFINEDthis refinedType_ASTRef | |||
| SKOLEMtype Type_ASTRef | |||
There was a problem hiding this comment.
When can Skolems appear in typed trees?
There was a problem hiding this comment.
They will be removed in a separate PR (#638).
|
Could this new |
|
@smarter They are still different. In Applications, we need a TermRef for the method reference, which is what the newSkolem enables. SkolemType does not provide us with a method symbol. |
|
Would be great to see a review of this so we can get this in. |
|
I am merging now, because the commit fixes an important unsoundness problem in Dotty. The longer we leave this open the more likely it is that other commits will introduce unsound code. |
Tighten comparison of skolem types
Skolem types are =:= only if they are reference-equal. Two skolem types
with the same underlying type are not necessarily equal.
Tests continue to run under this tightened definition.
No review necessary yet. More commits will follow.