Skip to content

Commit bd089c6

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 698a854 commit bd089c6

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 {
@@ -175,6 +182,29 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
175182
}
176183
}
177184

185+
private def isSubApproxLo(tp1: Type, tp2: Type) = {
186+
val saved = loIsPrecise
187+
loIsPrecise = false
188+
try isSubType(tp1, tp2) finally loIsPrecise = saved
189+
}
190+
191+
private def isSubApproxHi(tp1: Type, tp2: Type) = {
192+
val saved = hiIsPrecise
193+
hiIsPrecise = false
194+
try isSubType(tp1, tp2) finally hiIsPrecise = saved
195+
}
196+
197+
private def isSubTypePart(tp1: Type, tp2: Type) = {
198+
val savedHi = hiIsPrecise
199+
val savedLo = loIsPrecise
200+
hiIsPrecise = true
201+
loIsPrecise = true
202+
try isSubType(tp1, tp2) finally {
203+
hiIsPrecise = savedHi
204+
loIsPrecise = savedLo
205+
}
206+
}
207+
178208
private def firstTry(tp1: Type, tp2: Type): Boolean = tp2 match {
179209
case tp2: NamedType =>
180210
def compareNamed(tp1: Type, tp2: NamedType): Boolean = {
@@ -208,13 +238,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
208238
if ((sym1 ne NoSymbol) && (sym1 eq sym2))
209239
ctx.erasedTypes ||
210240
sym1.isStaticOwner ||
211-
isSubType(tp1.prefix, tp2.prefix) ||
241+
isSubTypePart(tp1.prefix, tp2.prefix) ||
212242
thirdTryNamed(tp1, tp2)
213243
else
214244
( (tp1.name eq tp2.name)
215245
&& tp1.isMemberRef
216246
&& tp2.isMemberRef
217-
&& isSubType(tp1.prefix, tp2.prefix)
247+
&& isSubTypePart(tp1.prefix, tp2.prefix)
218248
&& tp1.signature == tp2.signature
219249
&& !(sym1.isClass && sym2.isClass) // class types don't subtype each other
220250
) ||
@@ -270,7 +300,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
270300
}
271301
compareSuper
272302
case AndType(tp21, tp22) =>
273-
isSubType(tp1, tp21) && isSubType(tp1, tp22)
303+
isSubType(tp1, tp21) && isSubType(tp1, tp22) // no isSubApprox, as the two calls together maintain all information
274304
case OrType(tp21, tp22) =>
275305
if (tp21.stripTypeVar eq tp22.stripTypeVar) isSubType(tp1, tp21)
276306
else secondTry(tp1, tp2)
@@ -293,6 +323,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
293323
secondTry(tp1, tp2)
294324
}
295325

326+
def testConstrain(tp1: Type, tp2: Type, isUpper: Boolean): Boolean =
327+
!newScheme ||
328+
(if (isUpper) hiIsPrecise else loIsPrecise) || {
329+
println(i"missing constraint $tp1 with $tp2, isUpper = $isUpper")
330+
false
331+
}
332+
296333
private def secondTry(tp1: Type, tp2: Type): Boolean = tp1 match {
297334
case tp1: NamedType =>
298335
tp1.info match {
@@ -314,7 +351,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
314351
def compareTypeParamRef =
315352
ctx.mode.is(Mode.TypevarsMissContext) ||
316353
isSubTypeWhenFrozen(bounds(tp1).hi, tp2) || {
317-
if (canConstrain(tp1)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
354+
if (canConstrain(tp1) && testConstrain(tp1, tp2, isUpper = true)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
318355
else thirdTry(tp1, tp2)
319356
}
320357
compareTypeParamRef
@@ -379,8 +416,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
379416
GADTusage(tp2.symbol)
380417
}
381418
val tryLowerFirst = frozenConstraint || !isCappable(tp1)
382-
if (tryLowerFirst) isSubType(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
383-
else compareGADT || fourthTry(tp1, tp2) || isSubType(tp1, lo2)
419+
if (tryLowerFirst) isSubApproxHi(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
420+
else compareGADT || fourthTry(tp1, tp2) || isSubApproxHi(tp1, lo2)
384421

385422
case _ =>
386423
val cls2 = tp2.symbol
@@ -393,7 +430,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
393430
if (cls2.is(JavaDefined))
394431
// If `cls2` is parameterized, we are seeing a raw type, so we need to compare only the symbol
395432
return base.typeSymbol == cls2
396-
if (base ne tp1) return isSubType(base, tp2)
433+
if (base ne tp1)
434+
return if (tp1.isRef(cls2)) isSubType(base, tp2) else isSubApproxLo(base, tp2)
397435
}
398436
if (cls2 == defn.SingletonClass && tp1.isStable) return true
399437
}
@@ -420,7 +458,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
420458
if (frozenConstraint) isSubType(tp1, bounds(tp2).lo)
421459
else isSubTypeWhenFrozen(tp1, tp2)
422460
alwaysTrue || {
423-
if (canConstrain(tp2)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
461+
if (canConstrain(tp2) && testConstrain(tp2, tp1.widenExpr, isUpper = false)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
424462
else fourthTry(tp1, tp2)
425463
}
426464
}
@@ -481,14 +519,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
481519
def boundsOK =
482520
ctx.scala2Mode ||
483521
tp1.typeParams.corresponds(tp2.typeParams)((tparam1, tparam2) =>
484-
isSubType(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
522+
isSubTypePart(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
485523
val saved = comparedTypeLambdas
486524
comparedTypeLambdas += tp1
487525
comparedTypeLambdas += tp2
488526
try
489527
variancesConform(tp1.typeParams, tp2.typeParams) &&
490528
boundsOK &&
491-
isSubType(tp1.resType, tp2.resType.subst(tp2, tp1))
529+
isSubTypePart(tp1.resType, tp2.resType.subst(tp2, tp1))
492530
finally comparedTypeLambdas = saved
493531
case _ =>
494532
if (tp1.isHK) {
@@ -535,7 +573,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
535573
(tp1.signature consistentParams tp2.signature) &&
536574
matchingParams(tp1, tp2) &&
537575
(!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
538-
isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
576+
isSubTypePart(tp1.resultType, tp2.resultType.subst(tp2, tp1))
539577
case _ =>
540578
false
541579
}
@@ -548,15 +586,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
548586
// as members of the same type. And it seems most logical to take
549587
// ()T <:< => T, since everything one can do with a => T one can
550588
// also do with a ()T by automatic () insertion.
551-
case tp1 @ MethodType(Nil) => isSubType(tp1.resultType, restpe2)
552-
case _ => isSubType(tp1.widenExpr, restpe2)
589+
case tp1 @ MethodType(Nil) => isSubTypePart(tp1.resultType, restpe2)
590+
case _ => isSubTypePart(tp1.widenExpr, restpe2)
553591
}
554592
compareExpr
555593
case tp2 @ TypeBounds(lo2, hi2) =>
556594
def compareTypeBounds = tp1 match {
557595
case tp1 @ TypeBounds(lo1, hi1) =>
558-
((lo2 eq NothingType) || isSubType(lo2, lo1)) &&
559-
((hi2 eq AnyType) || isSubType(hi1, hi2))
596+
((lo2 eq NothingType) || isSubTypePart(lo2, lo1)) &&
597+
((hi2 eq AnyType) || isSubTypePart(hi1, hi2))
560598
case tp1: ClassInfo =>
561599
tp2 contains tp1
562600
case _ =>
@@ -566,7 +604,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
566604
case ClassInfo(pre2, cls2, _, _, _) =>
567605
def compareClassInfo = tp1 match {
568606
case ClassInfo(pre1, cls1, _, _, _) =>
569-
(cls1 eq cls2) && isSubType(pre1, pre2)
607+
(cls1 eq cls2) && isSubTypePart(pre1, pre2)
570608
case _ =>
571609
false
572610
}
@@ -586,7 +624,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
586624
narrowGADTBounds(tp1, tp2, isUpper = true)) &&
587625
GADTusage(tp1.symbol)
588626
}
589-
isSubType(hi1, tp2) || compareGADT
627+
isSubApproxLo(hi1, tp2) || compareGADT
590628
case _ =>
591629
def isNullable(tp: Type): Boolean = tp.widenDealias match {
592630
case tp: TypeRef => tp.symbol.isNullableClass
@@ -627,7 +665,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
627665
case EtaExpansion(tycon1) => isSubType(tycon1, tp2)
628666
case _ => tp2 match {
629667
case tp2: HKTypeLambda => false // this case was covered in thirdTry
630-
case _ => tp2.isHK && isSubType(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
668+
case _ => tp2.isHK && isSubTypePart(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
631669
}
632670
}
633671
compareHKLambda
@@ -654,7 +692,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
654692
either(isSubType(tp11, tp2), isSubType(tp12, tp2))
655693
case JavaArrayType(elem1) =>
656694
def compareJavaArray = tp2 match {
657-
case JavaArrayType(elem2) => isSubType(elem1, elem2)
695+
case JavaArrayType(elem2) => isSubTypePart(elem1, elem2)
658696
case _ => tp2 isRef ObjectClass
659697
}
660698
compareJavaArray
@@ -685,7 +723,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
685723
case tycon1: TypeRef =>
686724
tycon2.dealias match {
687725
case tycon2: TypeRef if tycon1.symbol == tycon2.symbol =>
688-
isSubType(tycon1.prefix, tycon2.prefix) &&
726+
isSubTypePart(tycon1.prefix, tycon2.prefix) &&
689727
isSubArgs(args1, args2, tp1, tparams)
690728
case _ =>
691729
false
@@ -766,7 +804,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
766804
* @param tyconLo The type constructor's lower approximation.
767805
*/
768806
def fallback(tyconLo: Type) =
769-
either(fourthTry(tp1, tp2), isSubType(tp1, tyconLo.applyIfParameterized(args2)))
807+
either(fourthTry(tp1, tp2), isSubApproxHi(tp1, tyconLo.applyIfParameterized(args2)))
770808

771809
/** Let `tycon2bounds` be the bounds of the RHS type constructor `tycon2`.
772810
* Let `app2 = tp2` where the type constructor of `tp2` is replaced by
@@ -779,9 +817,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
779817
*/
780818
def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
781819
if (tycon2bounds.lo eq tycon2bounds.hi)
782-
isSubType(tp1,
783-
if (tyconIsTypeRef) tp2.superType
784-
else tycon2bounds.lo.applyIfParameterized(args2))
820+
if (tyconIsTypeRef) isSubType(tp1, tp2.superType)
821+
else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2))
785822
else
786823
fallback(tycon2bounds.lo)
787824

@@ -797,7 +834,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
797834
compareLower(info2, tyconIsTypeRef = true)
798835
case info2: ClassInfo =>
799836
val base = tp1.baseType(info2.cls)
800-
if (base.exists && base.ne(tp1)) isSubType(base, tp2)
837+
if (base.exists && base.ne(tp1))
838+
if (tp1.isRef(info2.cls)) isSubType(base, tp2)
839+
else isSubApproxLo(base, tp2)
801840
else fourthTry(tp1, tp2)
802841
case _ =>
803842
fourthTry(tp1, tp2)
@@ -824,7 +863,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
824863
false
825864
}
826865
canConstrain(param1) && canInstantiate ||
827-
isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2)
866+
isSubApproxLo(bounds(param1).hi.applyIfParameterized(args1), tp2)
828867
case tycon1: TypeRef if tycon1.symbol.isClass =>
829868
false
830869
case tycon1: TypeProxy =>
@@ -858,8 +897,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
858897
case arg1: TypeBounds =>
859898
compareCaptured(arg1, arg2)
860899
case _ =>
861-
(v > 0 || isSubType(arg2, arg1)) &&
862-
(v < 0 || isSubType(arg1, arg2))
900+
(v > 0 || isSubTypePart(arg2, arg1)) &&
901+
(v < 0 || isSubTypePart(arg1, arg2))
863902
}
864903
}
865904

@@ -962,7 +1001,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
9621001
if (isCovered(tp1) && isCovered(tp2)) {
9631002
//println(s"useless subtype: $tp1 <:< $tp2")
9641003
false
965-
} else isSubType(tp1, tp2)
1004+
} else isSubApproxLo(tp1, tp2)
9661005

9671006
/** Does type `tp1` have a member with name `name` whose normalized type is a subtype of
9681007
* the normalized type of the refinement `tp2`?
@@ -991,15 +1030,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
9911030
tp2.refinedInfo match {
9921031
case rinfo2: TypeBounds =>
9931032
val ref1 = tp1.widenExpr.select(name)
994-
isSubType(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
1033+
isSubTypePart(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
9951034
case _ =>
9961035
false
9971036
}
9981037
case _ => false
9991038
}
10001039

10011040
def qualifies(m: SingleDenotation) =
1002-
isSubType(m.info, rinfo2) || matchAbstractTypeMember(m.info)
1041+
isSubTypePart(m.info, rinfo2) || matchAbstractTypeMember(m.info)
10031042

10041043
tp1.member(name) match { // inlined hasAltWith for performance
10051044
case mbr: SingleDenotation => qualifies(mbr)
@@ -1039,7 +1078,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10391078
*/
10401079
private def isSubRefinements(tp1: RefinedType, tp2: RefinedType, limit: Type): Boolean = {
10411080
def hasSubRefinement(tp1: RefinedType, refine2: Type): Boolean = {
1042-
isSubType(tp1.refinedInfo, refine2) || {
1081+
isSubTypePart(tp1.refinedInfo, refine2) || {
10431082
// last effort: try to adapt variances of higher-kinded types if this is sound.
10441083
// TODO: Move this to eta-expansion?
10451084
val adapted2 = refine2.adaptHkVariances(tp1.parent.member(tp1.refinedName).symbol.info)
@@ -1079,7 +1118,6 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10791118
* case of a GADT bounded typeref, we should narrow with `tp2` instead of its lower bound.
10801119
*/
10811120
private def isCappable(tp: Type): Boolean = tp match {
1082-
case tp: TypeRef => ctx.gadt.bounds.contains(tp.symbol)
10831121
case tp: TypeParamRef => constraint contains tp
10841122
case tp: TypeProxy => isCappable(tp.underlying)
10851123
case tp: AndOrType => isCappable(tp.tp1) || isCappable(tp.tp2)
@@ -1090,8 +1128,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10901128
* `bound` as an upper or lower bound (which depends on `isUpper`).
10911129
* Test that the resulting bounds are still satisfiable.
10921130
*/
1093-
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean =
1094-
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && {
1131+
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean = {
1132+
val boundIsPrecise = if (isUpper) hiIsPrecise else loIsPrecise
1133+
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && boundIsPrecise && {
10951134
val tparam = tr.symbol
10961135
gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
10971136
if (bound.isRef(tparam)) false
@@ -1100,10 +1139,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
11001139
val newBounds =
11011140
if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound)
11021141
else TypeBounds(oldBounds.lo | bound, oldBounds.hi)
1103-
isSubType(newBounds.lo, newBounds.hi) &&
1142+
isSubTypePart(newBounds.lo, newBounds.hi) &&
11041143
{ ctx.gadt.setBounds(tparam, newBounds); true }
11051144
}
11061145
}
1146+
}
11071147

11081148
// Tests around `matches`
11091149

0 commit comments

Comments
 (0)