Skip to content

Commit 1e91c94

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 4f24531 commit 1e91c94

File tree

1 file changed

+77
-37
lines changed

1 file changed

+77
-37
lines changed

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

Lines changed: 77 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
3030

3131
private[this] var needsGc = false
3232

33+
/** True iff a compared type `tp1` */
34+
private[this] var loIsPrecise = true
35+
private[this] var hiIsPrecise = true
36+
val newScheme = true
37+
3338
/** Is a subtype check in progress? In that case we may not
3439
* permanently instantiate type variables, because the corresponding
3540
* constraint might still be retracted and the instantiation should
@@ -111,7 +116,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
111116
}
112117
}
113118

114-
protected def isSubType(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)}", subtyping) {
119+
protected def isSubType(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $loIsPrecise $hiIsPrecise", subtyping) {
120+
//assert(s"isSubType ${traceInfo(tp1, tp2)} $loIsPrecise $hiIsPrecise" !=
121+
// "isSubType String <:< E false true")
115122
if (tp2 eq NoType) false
116123
else if (tp1 eq tp2) true
117124
else {
@@ -179,6 +186,29 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
179186
}
180187
}
181188

189+
private def isSubApproxLo(tp1: Type, tp2: Type) = {
190+
val saved = loIsPrecise
191+
loIsPrecise = false
192+
try isSubType(tp1, tp2) finally loIsPrecise = saved
193+
}
194+
195+
private def isSubApproxHi(tp1: Type, tp2: Type) = {
196+
val saved = hiIsPrecise
197+
hiIsPrecise = false
198+
try isSubType(tp1, tp2) finally hiIsPrecise = saved
199+
}
200+
201+
private def isSubTypePart(tp1: Type, tp2: Type) = {
202+
val savedHi = hiIsPrecise
203+
val savedLo = loIsPrecise
204+
hiIsPrecise = true
205+
loIsPrecise = true
206+
try isSubType(tp1, tp2) finally {
207+
hiIsPrecise = savedHi
208+
loIsPrecise = savedLo
209+
}
210+
}
211+
182212
private def firstTry(tp1: Type, tp2: Type): Boolean = tp2 match {
183213
case tp2: NamedType =>
184214
def compareNamed(tp1: Type, tp2: NamedType): Boolean = {
@@ -212,13 +242,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
212242
if ((sym1 ne NoSymbol) && (sym1 eq sym2))
213243
ctx.erasedTypes ||
214244
sym1.isStaticOwner ||
215-
isSubType(tp1.prefix, tp2.prefix) ||
245+
isSubTypePart(tp1.prefix, tp2.prefix) ||
216246
thirdTryNamed(tp1, tp2)
217247
else
218248
( (tp1.name eq tp2.name)
219249
&& tp1.isMemberRef
220250
&& tp2.isMemberRef
221-
&& isSubType(tp1.prefix, tp2.prefix)
251+
&& isSubTypePart(tp1.prefix, tp2.prefix)
222252
&& tp1.signature == tp2.signature
223253
&& !(sym1.isClass && sym2.isClass) // class types don't subtype each other
224254
) ||
@@ -274,7 +304,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
274304
}
275305
compareSuper
276306
case AndType(tp21, tp22) =>
277-
isSubType(tp1, tp21) && isSubType(tp1, tp22)
307+
isSubType(tp1, tp21) && isSubType(tp1, tp22) // no isSubApprox, as the two calls together maintain all information
278308
case OrType(tp21, tp22) =>
279309
if (tp21.stripTypeVar eq tp22.stripTypeVar) isSubType(tp1, tp21)
280310
else secondTry(tp1, tp2)
@@ -297,6 +327,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
297327
secondTry(tp1, tp2)
298328
}
299329

330+
def testConstrain(tp1: Type, tp2: Type, isUpper: Boolean): Boolean =
331+
!newScheme ||
332+
(if (isUpper) hiIsPrecise else loIsPrecise) || {
333+
println(i"missing constraint $tp1 with $tp2, isUpper = $isUpper")
334+
false
335+
}
336+
300337
private def secondTry(tp1: Type, tp2: Type): Boolean = tp1 match {
301338
case tp1: NamedType =>
302339
tp1.info match {
@@ -319,7 +356,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
319356
def compareTypeParamRef =
320357
ctx.mode.is(Mode.TypevarsMissContext) ||
321358
isSubTypeWhenFrozen(bounds(tp1).hi, tp2) || {
322-
if (canConstrain(tp1)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
359+
if (canConstrain(tp1) && testConstrain(tp1, tp2, isUpper = true)) addConstraint(tp1, tp2, fromBelow = false) && flagNothingBound
323360
else thirdTry(tp1, tp2)
324361
}
325362
compareTypeParamRef
@@ -384,8 +421,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
384421
GADTusage(tp2.symbol)
385422
}
386423
val tryLowerFirst = frozenConstraint || !isCappable(tp1)
387-
if (tryLowerFirst) isSubType(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
388-
else compareGADT || fourthTry(tp1, tp2) || isSubType(tp1, lo2)
424+
if (tryLowerFirst) isSubApproxHi(tp1, lo2) || compareGADT || fourthTry(tp1, tp2)
425+
else compareGADT || fourthTry(tp1, tp2) || isSubApproxHi(tp1, lo2)
389426

390427
case _ =>
391428
val cls2 = tp2.symbol
@@ -398,7 +435,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
398435
if (cls2.is(JavaDefined))
399436
// If `cls2` is parameterized, we are seeing a raw type, so we need to compare only the symbol
400437
return base.typeSymbol == cls2
401-
if (base ne tp1) return isSubType(base, tp2)
438+
if (base ne tp1)
439+
return if (tp1.isRef(cls2)) isSubType(base, tp2) else isSubApproxLo(base, tp2)
402440
}
403441
if (cls2 == defn.SingletonClass && tp1.isStable) return true
404442
}
@@ -425,7 +463,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
425463
if (frozenConstraint) isSubType(tp1, bounds(tp2).lo)
426464
else isSubTypeWhenFrozen(tp1, tp2)
427465
alwaysTrue || {
428-
if (canConstrain(tp2)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
466+
if (canConstrain(tp2) && testConstrain(tp2, tp1.widenExpr, isUpper = false)) addConstraint(tp2, tp1.widenExpr, fromBelow = true)
429467
else fourthTry(tp1, tp2)
430468
}
431469
}
@@ -486,14 +524,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
486524
def boundsOK =
487525
ctx.scala2Mode ||
488526
tp1.typeParams.corresponds(tp2.typeParams)((tparam1, tparam2) =>
489-
isSubType(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
527+
isSubTypePart(tparam2.paramInfo.subst(tp2, tp1), tparam1.paramInfo))
490528
val saved = comparedTypeLambdas
491529
comparedTypeLambdas += tp1
492530
comparedTypeLambdas += tp2
493531
try
494532
variancesConform(tp1.typeParams, tp2.typeParams) &&
495533
boundsOK &&
496-
isSubType(tp1.resType, tp2.resType.subst(tp2, tp1))
534+
isSubTypePart(tp1.resType, tp2.resType.subst(tp2, tp1))
497535
finally comparedTypeLambdas = saved
498536
case _ =>
499537
if (tp1.isHK) {
@@ -540,7 +578,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
540578
(tp1.signature consistentParams tp2.signature) &&
541579
matchingParams(tp1, tp2) &&
542580
(!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
543-
isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
581+
isSubTypePart(tp1.resultType, tp2.resultType.subst(tp2, tp1))
544582
case _ =>
545583
false
546584
}
@@ -553,15 +591,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
553591
// as members of the same type. And it seems most logical to take
554592
// ()T <:< => T, since everything one can do with a => T one can
555593
// also do with a ()T by automatic () insertion.
556-
case tp1 @ MethodType(Nil) => isSubType(tp1.resultType, restpe2)
557-
case _ => isSubType(tp1.widenExpr, restpe2)
594+
case tp1 @ MethodType(Nil) => isSubTypePart(tp1.resultType, restpe2)
595+
case _ => isSubTypePart(tp1.widenExpr, restpe2)
558596
}
559597
compareExpr
560598
case tp2 @ TypeBounds(lo2, hi2) =>
561599
def compareTypeBounds = tp1 match {
562600
case tp1 @ TypeBounds(lo1, hi1) =>
563-
((lo2 eq NothingType) || isSubType(lo2, lo1)) &&
564-
((hi2 eq AnyType) || isSubType(hi1, hi2))
601+
((lo2 eq NothingType) || isSubTypePart(lo2, lo1)) &&
602+
((hi2 eq AnyType) || isSubTypePart(hi1, hi2))
565603
case tp1: ClassInfo =>
566604
tp2 contains tp1
567605
case _ =>
@@ -571,7 +609,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
571609
case ClassInfo(pre2, cls2, _, _, _) =>
572610
def compareClassInfo = tp1 match {
573611
case ClassInfo(pre1, cls1, _, _, _) =>
574-
(cls1 eq cls2) && isSubType(pre1, pre2)
612+
(cls1 eq cls2) && isSubTypePart(pre1, pre2)
575613
case _ =>
576614
false
577615
}
@@ -591,7 +629,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
591629
narrowGADTBounds(tp1, tp2, isUpper = true)) &&
592630
GADTusage(tp1.symbol)
593631
}
594-
isSubType(hi1, tp2) || compareGADT
632+
isSubApproxLo(hi1, tp2) || compareGADT
595633
case _ =>
596634
def isNullable(tp: Type): Boolean = tp.widenDealias match {
597635
case tp: TypeRef => tp.symbol.isNullableClass
@@ -632,7 +670,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
632670
case EtaExpansion(tycon1) => isSubType(tycon1, tp2)
633671
case _ => tp2 match {
634672
case tp2: HKTypeLambda => false // this case was covered in thirdTry
635-
case _ => tp2.isHK && isSubType(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
673+
case _ => tp2.isHK && isSubTypePart(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
636674
}
637675
}
638676
compareHKLambda
@@ -659,7 +697,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
659697
either(isSubType(tp11, tp2), isSubType(tp12, tp2))
660698
case JavaArrayType(elem1) =>
661699
def compareJavaArray = tp2 match {
662-
case JavaArrayType(elem2) => isSubType(elem1, elem2)
700+
case JavaArrayType(elem2) => isSubTypePart(elem1, elem2)
663701
case _ => tp2 isRef ObjectClass
664702
}
665703
compareJavaArray
@@ -690,7 +728,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
690728
case tycon1: TypeRef =>
691729
tycon2.dealias match {
692730
case tycon2: TypeRef if tycon1.symbol == tycon2.symbol =>
693-
isSubType(tycon1.prefix, tycon2.prefix) &&
731+
isSubTypePart(tycon1.prefix, tycon2.prefix) &&
694732
isSubArgs(args1, args2, tp1, tparams)
695733
case _ =>
696734
false
@@ -771,7 +809,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
771809
* @param tyconLo The type constructor's lower approximation.
772810
*/
773811
def fallback(tyconLo: Type) =
774-
either(fourthTry(tp1, tp2), isSubType(tp1, tyconLo.applyIfParameterized(args2)))
812+
either(fourthTry(tp1, tp2), isSubApproxHi(tp1, tyconLo.applyIfParameterized(args2)))
775813

776814
/** Let `tycon2bounds` be the bounds of the RHS type constructor `tycon2`.
777815
* Let `app2 = tp2` where the type constructor of `tp2` is replaced by
@@ -784,9 +822,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
784822
*/
785823
def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
786824
if (tycon2bounds.lo eq tycon2bounds.hi)
787-
isSubType(tp1,
788-
if (tyconIsTypeRef) tp2.superType
789-
else tycon2bounds.lo.applyIfParameterized(args2))
825+
if (tyconIsTypeRef) isSubType(tp1, tp2.superType)
826+
else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2))
790827
else
791828
fallback(tycon2bounds.lo)
792829

@@ -802,7 +839,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
802839
compareLower(info2, tyconIsTypeRef = true)
803840
case info2: ClassInfo =>
804841
val base = tp1.baseType(info2.cls)
805-
if (base.exists && base.ne(tp1)) isSubType(base, tp2)
842+
if (base.exists && base.ne(tp1))
843+
if (tp1.isRef(info2.cls)) isSubType(base, tp2)
844+
else isSubApproxLo(base, tp2)
806845
else fourthTry(tp1, tp2)
807846
case _ =>
808847
fourthTry(tp1, tp2)
@@ -829,7 +868,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
829868
false
830869
}
831870
canConstrain(param1) && canInstantiate ||
832-
isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2)
871+
isSubApproxLo(bounds(param1).hi.applyIfParameterized(args1), tp2)
833872
case tycon1: TypeRef if tycon1.symbol.isClass =>
834873
false
835874
case tycon1: TypeProxy =>
@@ -863,8 +902,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
863902
case arg1: TypeBounds =>
864903
compareCaptured(arg1, arg2)
865904
case _ =>
866-
(v > 0 || isSubType(arg2, arg1)) &&
867-
(v < 0 || isSubType(arg1, arg2))
905+
(v > 0 || isSubTypePart(arg2, arg1)) &&
906+
(v < 0 || isSubTypePart(arg1, arg2))
868907
}
869908
}
870909

@@ -967,7 +1006,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
9671006
if (isCovered(tp1) && isCovered(tp2)) {
9681007
//println(s"useless subtype: $tp1 <:< $tp2")
9691008
false
970-
} else isSubType(tp1, tp2)
1009+
} else isSubApproxLo(tp1, tp2)
9711010

9721011
/** Does type `tp1` have a member with name `name` whose normalized type is a subtype of
9731012
* the normalized type of the refinement `tp2`?
@@ -996,15 +1035,15 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
9961035
tp2.refinedInfo match {
9971036
case rinfo2: TypeBounds =>
9981037
val ref1 = tp1.widenExpr.select(name)
999-
isSubType(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
1038+
isSubTypePart(rinfo2.lo, ref1) && isSubType(ref1, rinfo2.hi)
10001039
case _ =>
10011040
false
10021041
}
10031042
case _ => false
10041043
}
10051044

10061045
def qualifies(m: SingleDenotation) =
1007-
isSubType(m.info, rinfo2) || matchAbstractTypeMember(m.info)
1046+
isSubTypePart(m.info, rinfo2) || matchAbstractTypeMember(m.info)
10081047

10091048
tp1.member(name) match { // inlined hasAltWith for performance
10101049
case mbr: SingleDenotation => qualifies(mbr)
@@ -1044,7 +1083,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10441083
*/
10451084
private def isSubRefinements(tp1: RefinedType, tp2: RefinedType, limit: Type): Boolean = {
10461085
def hasSubRefinement(tp1: RefinedType, refine2: Type): Boolean = {
1047-
isSubType(tp1.refinedInfo, refine2) || {
1086+
isSubTypePart(tp1.refinedInfo, refine2) || {
10481087
// last effort: try to adapt variances of higher-kinded types if this is sound.
10491088
// TODO: Move this to eta-expansion?
10501089
val adapted2 = refine2.adaptHkVariances(tp1.parent.member(tp1.refinedName).symbol.info)
@@ -1084,7 +1123,6 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10841123
* case of a GADT bounded typeref, we should narrow with `tp2` instead of its lower bound.
10851124
*/
10861125
private def isCappable(tp: Type): Boolean = tp match {
1087-
case tp: TypeRef => ctx.gadt.bounds.contains(tp.symbol)
10881126
case tp: TypeParamRef => constraint contains tp
10891127
case tp: TypeProxy => isCappable(tp.underlying)
10901128
case tp: AndOrType => isCappable(tp.tp1) || isCappable(tp.tp2)
@@ -1095,8 +1133,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
10951133
* `bound` as an upper or lower bound (which depends on `isUpper`).
10961134
* Test that the resulting bounds are still satisfiable.
10971135
*/
1098-
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean =
1099-
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && {
1136+
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean = {
1137+
val boundIsPrecise = if (isUpper) hiIsPrecise else loIsPrecise
1138+
ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && boundIsPrecise && {
11001139
val tparam = tr.symbol
11011140
gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
11021141
if (bound.isRef(tparam)) false
@@ -1105,10 +1144,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
11051144
val newBounds =
11061145
if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound)
11071146
else TypeBounds(oldBounds.lo | bound, oldBounds.hi)
1108-
isSubType(newBounds.lo, newBounds.hi) &&
1147+
isSubTypePart(newBounds.lo, newBounds.hi) &&
11091148
{ ctx.gadt.setBounds(tparam, newBounds); true }
11101149
}
11111150
}
1151+
}
11121152

11131153
// Tests around `matches`
11141154

0 commit comments

Comments
 (0)