Skip to content

A more flexible scheme for handling the universal capability #18699

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 85 commits into from
Oct 23, 2023
Merged
Changes from 1 commit
Commits
Show all changes
85 commits
Select commit Hold shift + click to select a range
fce355e
Refine "cannot have inferred type" test
odersky Sep 13, 2023
1f94a68
Run Setup code one phase before CheckCaptures
odersky Sep 18, 2023
5c6a7fd
Don't shorten local roots when printing
odersky Sep 18, 2023
434f455
Drop rhsClosure from CCState
odersky Sep 18, 2023
1164d55
Fix computation of level owners
odersky Sep 19, 2023
2397cd7
Setup newScheme mechanism
odersky Sep 19, 2023
bf9a0b0
Introduce rootTarget for mapRoots customization
odersky Sep 19, 2023
62120fb
Change result type inference of vals and defs
odersky Sep 19, 2023
f550272
Make RecheckDef return a type
odersky Sep 19, 2023
aa29559
Use a separate phase to add try owners
odersky Sep 19, 2023
1a65114
Transform infos of all symbols defined in current run in SymTransformer
odersky Sep 20, 2023
f9d8b74
Fix bug when restoring denotations in Recheck.
odersky Sep 20, 2023
eb8457b
Do fluidify when transforming symbols instead of on access
odersky Sep 20, 2023
174ccb4
Align rechecking ValDefs and DefDefs
odersky Sep 20, 2023
e6c43c1
Revise inferred type checking
odersky Sep 20, 2023
ba1e919
Take singleton types into account when instantiating local roots
odersky Sep 21, 2023
622c73c
Replace some uses of CaptureSet universal to account for local roots
odersky Sep 21, 2023
baf530f
Less forcing of info when printing
odersky Sep 21, 2023
8a332f7
Also set CaptureChecked status for unpickled roots
odersky Sep 23, 2023
d8f8c5a
Let vals be lever owners
odersky Sep 23, 2023
4323b5b
Refactor wellformed checks
odersky Sep 23, 2023
99e3fe3
Drop boxedUnlessFun and boxedIfTypeParam operations
odersky Sep 23, 2023
3544db4
Fix followAlias
odersky Sep 25, 2023
c1f198e
Also interpolate root variables in non-variable capture sets.
odersky Sep 26, 2023
19a1fa7
Refactor addNewElems
odersky Sep 27, 2023
c933a74
Refactor level error reporting
odersky Sep 27, 2023
764302d
Make CompareResult an enum
odersky Sep 29, 2023
70ffa24
Add takesCappedParam criterion to isLevelOwner
odersky Sep 29, 2023
8a8765d
Decorate inferred type aliases as inferred types
odersky Sep 29, 2023
bbde15f
Setup correct environment when completing definitions
odersky Oct 1, 2023
cbd0e0c
Treat classes with universal self types as level owners
odersky Oct 1, 2023
f79e6ae
Revamp capture roots and captureset vars
odersky Oct 1, 2023
d38c7bd
Make RefiningVars level polymorphic
odersky Oct 1, 2023
8394962
Enable takesCappedParam criterion for level ownership
odersky Oct 1, 2023
fdabd8a
Use LooseCaptureRoot checking for checking bounds of applied types
odersky Oct 1, 2023
6da11f7
Update tests can check files
odersky Oct 1, 2023
568867a
Revert "Use LooseCaptureRoot checking for checking bounds of applied …
odersky Oct 1, 2023
4e67d95
Simplification: drop ccNestingLevel
odersky Oct 1, 2023
b8b94d3
Add @sharable annotation to global counter
odersky Oct 1, 2023
7b04b70
Handle outer class roots when instantiating class members
odersky Oct 3, 2023
c0b8fb5
Simplifications
odersky Oct 5, 2023
3fc63fc
Make constructors level owners
odersky Oct 5, 2023
a4e47b1
Work capture root determination into AsSeenFrom
odersky Oct 6, 2023
dac35e1
Keep track of failure traces when subCapturing fails under -Ycc-debug
odersky Oct 7, 2023
c769305
Keep track of enclosing capture sets when comparing refined types
odersky Oct 7, 2023
5423541
Change owner of computed capture set for constructor applications
odersky Oct 7, 2023
8a679aa
Treat added class refinements as inferred types for further processing
odersky Oct 7, 2023
b62e550
A first attempt at level checking for classes
odersky Oct 7, 2023
71f7478
Drop instantiateOuterClassRoots
odersky Oct 8, 2023
0fbd6b8
Disable some special cases about RefiningVars
odersky Oct 8, 2023
09f00bb
Introduce isCaptureChecking test
odersky Oct 8, 2023
c9a02c8
Restrict isUncachable
odersky Oct 8, 2023
c78df14
Move most of self type setup to transformSym
odersky Oct 9, 2023
388349a
Make non-final impure classes level owners
odersky Oct 9, 2023
9be0f6f
Translate local roots when doing override checks
odersky Oct 9, 2023
b3c4717
Map parents of classes with the class as owner.
odersky Oct 9, 2023
dd80312
Fix CC asSeenFrom when prefix is `this`
odersky Oct 9, 2023
6f9e565
Drop unnecessary code in transformSym
odersky Oct 10, 2023
ad43c66
Revert "Revert "Implement sealed type variables""
odersky Oct 12, 2023
c2b805a
Add adapation to convert global to local root
odersky Oct 13, 2023
1df49f1
Make cap a supercapture of local roots
odersky Oct 13, 2023
2be1b41
New scheme
odersky Oct 15, 2023
32f240d
Drop CaptureRoot and AddTryOwners
odersky Oct 15, 2023
16a2216
Drop redundant elements of Setup
odersky Oct 15, 2023
f786979
Drop BoxedTypeCache
odersky Oct 15, 2023
6a21e5f
Drop LooseRootCapturing
odersky Oct 15, 2023
2981ae7
Simplify TypeComparer
odersky Oct 15, 2023
9f82e69
Drop RefiningVar
odersky Oct 15, 2023
202445d
Captureset refactoring
odersky Oct 16, 2023
fc20b42
Failing test
odersky Oct 16, 2023
035786d
Add dropped test
odersky Oct 16, 2023
f6056ae
Drop other disabled tests
odersky Oct 16, 2023
88b328c
Merge AssignProto and LhProto
odersky Oct 16, 2023
2ae29fb
Fix box adaptation
Linyxus Oct 16, 2023
4ffbda9
Polish box adaptation for better legibility
odersky Oct 16, 2023
54aea78
Don't dealias TypeRefs when transforming explicit types
odersky Oct 17, 2023
ac8971e
Move all disallowRootCapabilitiesIn calls to checkCaptures
odersky Oct 17, 2023
d29d5e3
Simplify expandAliases
odersky Oct 18, 2023
c3b2f8a
Drop user-defined local roots
odersky Oct 18, 2023
a6624de
Polishing and change printing options
odersky Oct 18, 2023
eaccea3
Don't treat non-capturechecked classes are pure.
odersky Oct 19, 2023
8883176
In a BiMap variable, propagate backwards before trying to add the ele…
odersky Oct 20, 2023
20a9b96
Add captDebug printer
odersky Oct 20, 2023
2043885
Better error messages in healTypeParam
odersky Oct 21, 2023
181d96e
A more realistic test case
odersky Oct 21, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Keep track of enclosing capture sets when comparing refined types
When comparing refined types

   C{x: T}^cs  <:<  C{x: T'}^cs'

we need to remember the capture set `cs` on the left hand side when we
get to ask whether the refined type has a member `x: T'`, so that we
can correctly instantiate any local root `cap[C]` in the member type of `x`.
Same if the LHS is simply `C^cs`. In both cases we strip the capture set before
we get to take the compute `x`, so we have to re-add it at the point of that
member computation.
  • Loading branch information
odersky committed Oct 15, 2023
commit c769305d8c55663f266c76a1b74046ff043fe26d
70 changes: 52 additions & 18 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
private var myInstance: TypeComparer = this
def currentInstance: TypeComparer = myInstance

/** All capturing types in the original `tp1` enclosing the currently
* compared type.
*/
private var enclosingCapturing1: List[AnnotatedType] = Nil

/** Is a subtype check in progress? In that case we may not
* permanently instantiate type variables, because the corresponding
* constraint might still be retracted and the instantiation should
Expand Down Expand Up @@ -256,7 +261,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
report.log(explained(_.isSubType(tp1, tp2, approx)))
}
// Eliminate LazyRefs before checking whether we have seen a type before
val normalize = new TypeMap {
val normalize = new TypeMap with CaptureSet.IdempotentCaptRefMap {
val DerefLimit = 10
var derefCount = 0
def apply(t: Type) = t match {
Expand Down Expand Up @@ -538,17 +543,23 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling

res

case CapturingType(parent1, refs1) =>
if tp2.isAny then true
else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
|| !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
then
val tp2a =
if tp1.isBoxedCapturing && !parent1.isBoxedCapturing
then tp2.unboxed
else tp2
recur(parent1, tp2a)
else thirdTry
case tp1 @ CapturingType(parent1, refs1) =>
def compareCapturing =
if tp2.isAny then true
else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
|| !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
then
val tp2a =
if tp1.isBoxedCapturing && !parent1.isBoxedCapturing
then tp2.unboxed
else tp2
try
enclosingCapturing1 = tp1 :: enclosingCapturing1
recur(parent1, tp2a)
finally
enclosingCapturing1 = enclosingCapturing1.tail
else thirdTry
compareCapturing
case tp1: AnnotatedType if !tp1.isRefining =>
recur(tp1.parent, tp2)
case tp1: MatchType =>
Expand Down Expand Up @@ -660,10 +671,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case (info1: MethodType, info2: MethodType) =>
matchingMethodParams(info1, info2, precise = false)
&& isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
case (info1 @ CapturingType(parent1, refs1), info2: Type) =>
case (info1 @ CapturingType(parent1, refs1), info2: Type)
if info2.stripCapturing.isInstanceOf[MethodOrPoly] =>
subCaptures(refs1, info2.captureSet, frozenConstraint).isOK && sameBoxed(info1, info2, refs1)
&& isSubInfo(parent1, info2)
case (info1: Type, CapturingType(parent2, refs2)) =>
case (info1: Type, CapturingType(parent2, refs2))
if info1.stripCapturing.isInstanceOf[MethodOrPoly] =>
val refs1 = info1.captureSet
(refs1.isAlwaysEmpty || subCaptures(refs1, refs2, frozenConstraint).isOK) && sameBoxed(info1, info2, refs1)
&& isSubInfo(info1, parent2)
Expand All @@ -672,7 +685,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling

if defn.isFunctionType(tp2) then
if tp2.derivesFrom(defn.PolyFunctionClass) then
return isSubInfo(tp1.member(nme.apply).info, tp2.refinedInfo)
return isSubInfo(tp1.ccMember(nme.apply).info, tp2.refinedInfo)
else
tp1w.widenDealias match
case tp1: RefinedType =>
Expand Down Expand Up @@ -2028,7 +2041,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
* rebase both itself and the member info of `tp` on a freshly created skolem type.
*/
def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean =
trace(i"hasMatchingMember($tp1 . $name :? ${tp2.refinedInfo}), mbr: ${tp1.member(name).info}", subtyping) {
trace(i"hasMatchingMember($tp1 . $name :? ${tp2.refinedInfo}), mbr: ${tp1.ccMember(name).info}", subtyping) {

// If the member is an abstract type and the prefix is a path, compare the member itself
// instead of its bounds. This case is needed situations like:
Expand Down Expand Up @@ -2118,9 +2131,30 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
|| (tp1.isStable && m.symbol.isStableMember && isSubType(TermRef(tp1, m.symbol), tp2.refinedInfo))
end qualifies

tp1.member(name).hasAltWithInline(qualifies)
tp1.ccMember(name).hasAltWithInline(qualifies)
}

extension (qual: Type)
/** Add all directly enclosing capture sets to `qual` and select `name` on the
* resulting type. A capture set is directly enclosing if there is an enclosing
* capturing type with the set and all types between `qual` and that type
* are RefinedTypes or CapturingTypes.
*/
def ccMember(name: Name): Denotation =
def isEnclosing(tp: Type): Boolean = tp match
case RefinedType(parent, _, _) => isEnclosing(parent)
case CapturingType(parent, _) => isEnclosing(parent)
case _ => tp eq qual

def addCaptures(tp: Type, encls: List[AnnotatedType]): Type = encls match
case (ct @ CapturingType(parent, refs)) :: encls1 if isEnclosing(parent) =>
addCaptures(CapturingType(tp, refs, ct.isBoxedCapturing), encls1)
case _ =>
tp

addCaptures(qual, enclosingCapturing1).member(name)
end ccMember

final def ensureStableSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
case tp: SingletonType if tp.isStable => tp
case tp: ValueType => SkolemType(tp)
Expand Down Expand Up @@ -3397,7 +3431,7 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}

override def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean =
traceIndented(s"hasMatchingMember(${show(tp1)} . $name, ${show(tp2.refinedInfo)}), member = ${show(tp1.member(name).info)}") {
traceIndented(s"hasMatchingMember(${show(tp1)} . $name, ${show(tp2.refinedInfo)}), member = ${show(tp1.ccMember(name).info)}") {
super.hasMatchingMember(name, tp1, tp2)
}

Expand Down