Skip to content

Commit d9ce2e0

Browse files
oderskyodersky
committed
Keep track whether compared types are precise
Don't narrow GADT bounds or constraint if compared types are imprecise. Narrowing GADT bounds to imprecise types is unsound. Narrowing constraints to imprecise types loses possible types.
1 parent 6faeb58 commit d9ce2e0

File tree

1 file changed

+78
-38
lines changed

1 file changed

+78
-38
lines changed

‎compiler/src/dotty/tools/dotc/core/TypeComparer.scala

Lines changed: 78 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
2727

2828
private[this] var needsGc = false
2929

30+
/** True iff a compared type `tp1` */
31+
private[this] var loIsPrecise = true
32+
private[this] var hiIsPrecise = true
33+
val newScheme = true
34+
3035
/** Is a subtype check in progress? In that case we may not
3136
* permanently instantiate type variables, because the corresponding
3237
* constraint might still be retracted and the instantiation should
@@ -100,13 +105,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
100105
def topLevelSubType(tp1: Type, tp2: Type): Boolean = {
101106
if (tp2 eq NoType) return false
102107
if ((tp2 eq tp1) || (tp2 eq WildcardType)) return true
103-
try isSubType(tp1, tp2)
108+
try isSubTypePart(tp1, tp2)
104109
finally
105110
if (Config.checkConstraintsSatisfiable)
106111
assert(isSatisfiable, constraint.show)
107112
}
108113

109-
protected def isSubType(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)}", subtyping) {
114+
protected def isSubType(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $loIsPrecise $hiIsPrecise", subtyping) {
115+
//assert(s"isSubType ${traceInfo(tp1, tp2)} $loIsPrecise $hiIsPrecise" !=
116+
// "isSubType String <:< E false true")
110117
if (tp2 eq NoType) false
111118
else if (tp1 eq tp2) true
112119
else {
@@ -159,6 +166,29 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
159166
}
160167
}
161168

169+
private def isSubApproxLo(tp1: Type, tp2: Type) = {
170+
val saved = loIsPrecise
171+
loIsPrecise = false
172+
try isSubType(tp1, tp2) finally loIsPrecise = saved
173+
}
174+
175+
private def isSubApproxHi(tp1: Type, tp2: Type) = {
176+
val saved = hiIsPrecise
177+
hiIsPrecise = false
178+
try isSubType(tp1, tp2) finally hiIsPrecise = saved
179+
}
180+
181+
private def isSubTypePart(tp1: Type, tp2: Type) = {
182+
val savedHi = hiIsPrecise
183+
val savedLo = loIsPrecise
184+
hiIsPrecise = true
185+
loIsPrecise = true
186+
try isSubType(tp1, tp2) finally {
187+
hiIsPrecise = savedHi
188+
loIsPrecise = savedLo
189+
}
190+
}
191+
162192
private def firstTry(tp1: Type, tp2: Type): Boolean = tp2 match {
163193
case tp2: NamedType =>
164194
def compareNamed(tp1: Type, tp2: NamedType): Boolean = {
@@ -192,13 +222,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
192222
if ((sym1 ne NoSymbol) && (sym1 eq sym2))
193223
ctx.erasedTypes ||
194224
sym1.isStaticOwner ||
195-
isSubType(tp1.prefix, tp2.prefix) ||
225+
isSubTypePart(tp1.prefix, tp2.prefix) ||
196226
thirdTryNamed(tp1, tp2)
197227
else
198228
( (tp1.name eq tp2.name)
199229
&& tp1.isMemberRef
200230
&& tp2.isMemberRef
201-
&& isSubType(tp1.prefix, tp2.prefix)
231+
&& isSubTypePart(tp1.prefix, tp2.prefix)
202232
&& tp1.signature == tp2.signature
203233
&& !(sym1.isClass && sym2.isClass) // class types don't subtype each other
204234
) ||
@@ -254,7 +284,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
254284
}
255285
compareSuper
256286
case AndType(tp21, tp22) =>
257-
isSubType(tp1, tp21) && isSubType(tp1, tp22)
287+
isSubType(tp1, tp21) && isSubType(tp1, tp22) // no isSubApprox, as the two calls together maintain all information
258288
case OrType(tp21, tp22) =>
259289
if (tp21.stripTypeVar eq tp22.stripTypeVar) isSubType(tp1, tp21)
260290
else secondTry(tp1, tp2)
@@ -277,6 +307,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
277307
secondTry(tp1, tp2)
278308
}
279309

310+
def testConstrain(tp1: Type, tp2: Type, isUpper: Boolean): Boolean =
311+
!newScheme ||
312+
(if (isUpper) hiIsPrecise else loIsPrecise) || {
313+
println(i"missing constraint $tp1 with $tp2, isUpper = $isUpper")
314+
false
315+
}
316+
280317
private def secondTry(tp1: Type, tp2: Type): Boolean = tp1 match {
281318
case tp1: NamedType =>
282319
tp1.info match {
@@ -298,7 +335,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
298335
def compareTypeParamRef =
299336
ctx.mode.is(Mode.TypevarsMissContext) ||
300337
isSubTypeWhenFrozen(bounds(tp1).hi, tp2) || {
301-
if (canConstrain(tp1)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
338+
if (canConstrain(tp1) && testConstrain(tp1, tp2, isUpper = true)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
302339
else thirdTry(tp1, tp2)
303340
}
304341
compareTypeParamRef
@@ -363,8 +400,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
363400
GADTusage(tp2.symbol)
364401
}
365402
val tryLowerFirst = frozenConstraint || !isCappable(tp1)
366-
if (tryLowerFirst) isSubType(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
367-
else compareGADT || fourthTry(tp1, tp2) || isSubType(tp1, lo2)
403+
if (tryLowerFirst) isSubApproxHi(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
404+
else compareGADT || fourthTry(tp1, tp2) || isSubApproxHi(tp1, lo2)
368405

369406
case _ =>
370407
val cls2 = tp2.symbol
@@ -377,7 +414,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
377414
if (cls2.is(JavaDefined))
378415
// If `cls2` is parameterized, we are seeing a raw type, so we need to compare only the symbol
379416
return base.typeSymbol == cls2
380-
if (base ne tp1) return isSubType(base, tp2)
417+
if (base ne tp1)
418+
return if (tp1.isRef(cls2)) isSubType(base, tp2) else isSubApproxLo(base, tp2)
381419
}
382420
if (cls2 == defn.SingletonClass && tp1.isStable) return true
383421
}
@@ -404,7 +442,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
404442
if (frozenConstraint) isSubType(tp1, bounds(tp2).lo)
405443
else isSubTypeWhenFrozen(tp1, tp2)
406444
alwaysTrue || {
407-
if (canConstrain(tp2)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
445+
if (canConstrain(tp2) && testConstrain(tp2, tp1.widenExpr, isUpper = false)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
408446
else fourthTry(tp1, tp2)
409447
}
410448
}
@@ -465,14 +503,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
465503
def boundsOK =
466504
ctx.scala2Mode ||
467505
tp1.typeParams.corresponds(tp2.typeParams)((tparam1, tparam2) =>
468-
isSubType(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
506+
isSubTypePart(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
469507
val saved = comparedTypeLambdas
470508
comparedTypeLambdas += tp1
471509
comparedTypeLambdas += tp2
472510
try
473511
variancesConform(tp1.typeParams, tp2.typeParams) &&
474512
boundsOK &&
475-
isSubType(tp1.resType, tp2.resType.subst(tp2, tp1))
513+
isSubTypePart(tp1.resType, tp2.resType.subst(tp2, tp1))
476514
finally comparedTypeLambdas = saved
477515
case _ =>
478516
if (tp1.isHK) {
@@ -519,7 +557,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
519557
(tp1.signature consistentParams tp2.signature) &&
520558
matchingParams(tp1, tp2) &&
521559
(!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
522-
isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
560+
isSubTypePart(tp1.resultType, tp2.resultType.subst(tp2, tp1))
523561
case _ =>
524562
false
525563
}
@@ -532,15 +570,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
532570
// as members of the same type. And it seems most logical to take
533571
// ()T <:< => T, since everything one can do with a => T one can
534572
// also do with a ()T by automatic () insertion.
535-
case tp1 @ MethodType(Nil) => isSubType(tp1.resultType, restpe2)
536-
case _ => isSubType(tp1.widenExpr, restpe2)
573+
case tp1 @ MethodType(Nil) => isSubTypePart(tp1.resultType, restpe2)
574+
case _ => isSubTypePart(tp1.widenExpr, restpe2)
537575
}
538576
compareExpr
539577
case tp2 @ TypeBounds(lo2, hi2) =>
540578
def compareTypeBounds = tp1 match {
541579
case tp1 @ TypeBounds(lo1, hi1) =>
542-
((lo2 eq NothingType) || isSubType(lo2, lo1)) &&
543-
((hi2 eq AnyType) || isSubType(hi1, hi2))
580+
((lo2 eq NothingType) || isSubTypePart(lo2, lo1)) &&
581+
((hi2 eq AnyType) || isSubTypePart(hi1, hi2))
544582
case tp1: ClassInfo =>
545583
tp2 contains tp1
546584
case _ =>
@@ -550,7 +588,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
550588
case ClassInfo(pre2, cls2, _, _, _) =>
551589
def compareClassInfo = tp1 match {
552590
case ClassInfo(pre1, cls1, _, _, _) =>
553-
(cls1 eq cls2) && isSubType(pre1, pre2)
591+
(cls1 eq cls2) && isSubTypePart(pre1, pre2)
554592
case _ =>
555593
false
556594
}
@@ -570,7 +608,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
570608
narrowGADTBounds(tp1, tp2, isUpper = true)) &&
571609
GADTusage(tp1.symbol)
572610
}
573-
isSubType(hi1, tp2) || compareGADT
611+
isSubApproxLo(hi1, tp2) || compareGADT
574612
case _ =>
575613
def isNullable(tp: Type): Boolean = tp.widenDealias match {
576614
case tp: TypeRef => tp.symbol.isNullableClass
@@ -611,7 +649,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
611649
case EtaExpansion(tycon1) => isSubType(tycon1, tp2)
612650
case _ => tp2 match {
613651
case tp2: HKTypeLambda => false // this case was covered in thirdTry
614-
case _ => tp2.isHK && isSubType(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
652+
case _ => tp2.isHK && isSubTypePart(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
615653
}
616654
}
617655
compareHKLambda
@@ -638,7 +676,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
638676
either(isSubType(tp11, tp2), isSubType(tp12, tp2))
639677
case JavaArrayType(elem1) =>
640678
def compareJavaArray = tp2 match {
641-
case JavaArrayType(elem2) => isSubType(elem1, elem2)
679+
case JavaArrayType(elem2) => isSubTypePart(elem1, elem2)
642680
case _ => tp2 isRef ObjectClass
643681
}
644682
compareJavaArray
@@ -669,7 +707,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
669707
case tycon1: TypeRef =>
670708
tycon2.dealias match {
671709
case tycon2: TypeRef if tycon1.symbol == tycon2.symbol =>
672-
isSubType(tycon1.prefix, tycon2.prefix) &&
710+
isSubTypePart(tycon1.prefix, tycon2.prefix) &&
673711
isSubArgs(args1, args2, tp1, tparams)
674712
case _ =>
675713
false
@@ -750,7 +788,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
750788
* @param tyconLo The type constructor's lower approximation.
751789
*/
752790
def fallback(tyconLo: Type) =
753-
either(fourthTry(tp1, tp2), isSubType(tp1, tyconLo.applyIfParameterized(args2)))
791+
either(fourthTry(tp1, tp2), isSubApproxHi(tp1, tyconLo.applyIfParameterized(args2)))
754792

755793
/** Let `tycon2bounds` be the bounds of the RHS type constructor `tycon2`.
756794
* Let `app2 = tp2` where the type constructor of `tp2` is replaced by
@@ -763,9 +801,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
763801
*/
764802
def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
765803
if (tycon2bounds.lo eq tycon2bounds.hi)
766-
isSubType(tp1,
767-
if (tyconIsTypeRef) tp2.superType
768-
else tycon2bounds.lo.applyIfParameterized(args2))
804+
if (tyconIsTypeRef) isSubType(tp1, tp2.superType)
805+
else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2))
769806
else
770807
fallback(tycon2bounds.lo)
771808

@@ -781,7 +818,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
781818
compareLower(info2, tyconIsTypeRef = true)
782819
case info2: ClassInfo =>
783820
val base = tp1.baseType(info2.cls)
784-
if (base.exists && base.ne(tp1)) isSubType(base, tp2)
821+
if (base.exists && base.ne(tp1))
822+
if (tp1.isRef(info2.cls)) isSubType(base, tp2)
823+
else isSubApproxLo(base, tp2)
785824
else fourthTry(tp1, tp2)
786825
case _ =>
787826
fourthTry(tp1, tp2)
@@ -808,7 +847,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
808847
false
809848
}
810849
canConstrain(param1) && canInstantiate ||
811-
isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2)
850+
isSubApproxLo(bounds(param1).hi.applyIfParameterized(args1), tp2)
812851
case tycon1: TypeRef if tycon1.symbol.isClass =>
813852
false
814853
case tycon1: TypeProxy =>
@@ -842,8 +881,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
842881
case arg1: TypeBounds =>
843882
compareCaptured(arg1, arg2)
844883
case _ =>
845-
(v > 0 || isSubType(arg2, arg1)) &&
846-
(v < 0 || isSubType(arg1, arg2))
884+
(v > 0 || isSubTypePart(arg2, arg1)) &&
885+
(v < 0 || isSubTypePart(arg1, arg2))
847886
}
848887
}
849888

@@ -946,7 +985,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
946985
if (isCovered(tp1) && isCovered(tp2)) {
947986
//println(s"useless subtype: $tp1 <:< $tp2")
948987
false
949-
} else isSubType(tp1, tp2)
988+
} else isSubApproxLo(tp1, tp2)
950989

951990
/** Does type `tp1` have a member with name `name` whose normalized type is a subtype of
952991
* the normalized type of the refinement `tp2`?
@@ -975,15 +1014,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
9751014
tp2.refinedInfo match {
9761015
case rinfo2: TypeBounds =>
9771016
val ref1 = tp1.widenExpr.select(name)
978-
isSubType(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
1017+
isSubTypePart(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
9791018
case _ =>
9801019
false
9811020
}
9821021
case _ => false
9831022
}
9841023

9851024
def qualifies(m: SingleDenotation) =
986-
isSubType(m.info, rinfo2) || matchAbstractTypeMember(m.info)
1025+
isSubTypePart(m.info, rinfo2) || matchAbstractTypeMember(m.info)
9871026

9881027
tp1.member(name) match { // inlined hasAltWith for performance
9891028
case mbr: SingleDenotation => qualifies(mbr)
@@ -1023,7 +1062,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10231062
*/
10241063
private def isSubRefinements(tp1: RefinedType, tp2: RefinedType, limit: Type): Boolean = {
10251064
def hasSubRefinement(tp1: RefinedType, refine2: Type): Boolean = {
1026-
isSubType(tp1.refinedInfo, refine2) || {
1065+
isSubTypePart(tp1.refinedInfo, refine2) || {
10271066
// last effort: try to adapt variances of higher-kinded types if this is sound.
10281067
// TODO: Move this to eta-expansion?
10291068
val adapted2 = refine2.adaptHkVariances(tp1.parent.member(tp1.refinedName).symbol.info)
@@ -1063,7 +1102,6 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10631102
* case of a GADT bounded typeref, we should narrow with `tp2` instead of its lower bound.
10641103
*/
10651104
private def isCappable(tp: Type): Boolean = tp match {
1066-
case tp: TypeRef => ctx.gadt.bounds.contains(tp.symbol)
10671105
case tp: TypeParamRef => constraint contains tp
10681106
case tp: TypeProxy => isCappable(tp.underlying)
10691107
case tp: AndOrType => isCappable(tp.tp1) || isCappable(tp.tp2)
@@ -1074,8 +1112,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10741112
* `bound` as an upper or lower bound (which depends on `isUpper`).
10751113
* Test that the resulting bounds are still satisfiable.
10761114
*/
1077-
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean =
1078-
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && {
1115+
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean = {
1116+
val boundIsPrecise = if (isUpper) hiIsPrecise else loIsPrecise
1117+
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && boundIsPrecise && {
10791118
val tparam = tr.symbol
10801119
gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
10811120
if (bound.isRef(tparam)) false
@@ -1084,10 +1123,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10841123
val newBounds =
10851124
if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound)
10861125
else TypeBounds(oldBounds.lo | bound, oldBounds.hi)
1087-
isSubType(newBounds.lo, newBounds.hi) &&
1126+
isSubTypePart(newBounds.lo, newBounds.hi) &&
10881127
{ ctx.gadt.setBounds(tparam, newBounds); true }
10891128
}
10901129
}
1130+
}
10911131

10921132
// Tests around `matches`
10931133

0 commit comments

Comments
 (0)