From 6803ec696ee9905e78b237aaefe3e2c4f4078891 Mon Sep 17 00:00:00 2001 From: Eugene Flesselle Date: Fri, 12 Apr 2024 13:37:37 +0200 Subject: [PATCH 1/2] Improve ConstraintHandling of SkolemTypes by retaining instantiated type vars in LevelAvoidMap when possible. Fixes #19955 Consider pos/i19955a as an example. We try to adapt the given_IsInt_U for skolems of the form (?2 : Int) and (?7 : ?8.Out) where ?8 is an unknown value of type given_IsWrapOfInt_R[Int, Wrap[Int]], but only the former succeeds, even though ?8.Out is trivially within the bounds of U. The typing trace from the two implicit search results includes: ```scala [log typer] ==> typedImplicit(Cand(given_IsInt_U L4), IsInt[(?2 : Int)], , <399..399>)? [log typer] ==> isSubType(IsInt[U], IsInt[(?2 : Int)])? [log typer] ==> isSameType((?2 : Int), U)? [log typer] ==> isSubType((?2 : Int), U)? [log typer] <== isSubType((?2 : Int), U) = true [log typer] ==> isSubType(U, (?2 : Int))? [log typer] <== isSubType(U, (?2 : Int)) = true [log typer] <== isSameType((?2 : Int), U) = true [log typer] <== isSubType(IsInt[U], IsInt[(?2 : Int)]) = true [log typer] <== typedImplicit(Cand(given_IsInt_U L4), IsInt[(?2 : Int)], , <399..399>) = SearchSuccess: (given_IsInt_U : [U <: Int]: IsInt[U]) via given_IsInt_U[(?2 : Int)] [log typer] ==> typedImplicit(Cand(given_IsInt_U L4), IsInt[(?7 : ?8.Out)], , <423..423>)? [log typer] ==> isSubType(IsInt[U], IsInt[(?7 : ?8.Out)])? [log typer] ==> isSameType((?7 : ?8.Out), U)? [log typer] ==> isSubType((?7 : ?8.Out), U)? [log typer] <== isSubType((?7 : ?8.Out), U) = true [log typer] ==> isSubType(Int, (?7 : ?8.Out))? [log typer] <== isSubType(Int, (?7 : ?8.Out)) = false [log typer] <== isSameType((?7 : ?8.Out), U) = false [log typer] <== isSubType(IsInt[U], IsInt[(?7 : ?8.Out)]) = false [log typer] <== typedImplicit(Cand(given_IsInt_U L4), IsInt[(?7 : ?8.Out)], , <423..423>) = Search Failure: given_IsInt_U[U] ``` The difference in the failing case from the passing case is that the type variable U has been instantiated to Int by the first direction of isSameType before attempting the second direction. If we look closer at the ConstraintHandling: ``` [log typer] ==> addConstraint(U, (?2 : Int), true)? [log typer] ==> legalBound(U, (?2 : Int), false)? [log typer] ==> ApproximatingTypeMap#derivedSkolemType((?2 : Int), Int)? [log typer] <== ApproximatingTypeMap#derivedSkolemType((?2 : Int), Int) = (?2 : Int) [log typer] <== legalBound(U, (?2 : Int), false) = (?2 : Int) [log typer] ==> isSubType((?2 : Int), Int)? [log typer] <== isSubType((?2 : Int), Int) = true [log typer] <== addConstraint(U, (?2 : Int), true) = true [log typer] ==> addConstraint(U, (?7 : ?8.Out), true)? [log typer] ==> legalBound(U, (?7 : ?8.Out), false)? [log typer] ==> ApproximatingTypeMap#derivedSkolemType((?8 : given_IsWrapOfInt_R[Int, Wrap[Int]]), given_IsWrapOfInt_R[Int, Wrap[Int]])? [log typer] <== ApproximatingTypeMap#derivedSkolemType((?8 : given_IsWrapOfInt_R[Int, Wrap[Int]]), given_IsWrapOfInt_R[Int, Wrap[Int]]) = given_IsWrapOfInt_R[Int, Wrap[Int]] [log typer] ==> ApproximatingTypeMap#derivedSkolemType((?7 : ?8.Out), Int)? [log typer] <== ApproximatingTypeMap#derivedSkolemType((?7 : ?8.Out), Int) = Int [log typer] <== legalBound(U, (?7 : ?8.Out), false) = Int [log typer] <== addConstraint(U, (?7 : ?8.Out), true) = true ``` we can see that the issue lies in the approximation in the LevelAvoidMap used to obtain the legalBound. Modifying `ApproximatingTypeMap#derivedSkolemType` from `if info eq tp.info then tp`, to `if info frozen_=:= tp.info then tp.derivedSkolem(info)`, allows each direction of the subtyping checks in `isSameType` to obtain the more precise skolem as legal bound. But it does not solve the issue, since they obtain distinct skolems even if they equivalently-shaped, the constraints are still unsatisfiable. We can instead try to make `info eq tp.info` be true. It was not the case in the above example because `given_IsWrapOfInt_R[Int, Wrap[Int]]` contained a type variable `R := Wrap[Int]` which was substituted by the map. We can modify TypeMap to keep type variables rather than replace them by their instance when possible, i.e. when the instance is itself not transformed by the map. This solves the issue but breaks other places which assumed the stripping of type vars in TypeMaps. That problem is avoided by doing the changes in LevelAvoidMap only. [Cherry-picked f58cbf99fc38d698ae52a5f11b4e780225eec342] --- .../tools/dotc/core/ConstraintHandling.scala | 13 ++++++++- .../test/dotc/pos-test-pickling.blacklist | 3 +++ tests/pos/i19955a.scala | 27 +++++++++++++++++++ tests/pos/i19955b.scala | 17 ++++++++++++ tests/pos/i20053b.scala | 22 +++++++++++++++ 5 files changed, 81 insertions(+), 1 deletion(-) create mode 100644 tests/pos/i19955a.scala create mode 100644 tests/pos/i19955b.scala create mode 100644 tests/pos/i20053b.scala diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 64db5923bfea..c9c0db1609a7 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -240,7 +240,18 @@ trait ConstraintHandling { override def apply(tp: Type): Type = tp match case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) => legalVar(tp) - // TypeParamRef can occur in tl bounds + // TypeParamRef can occur in tl bounds + case tp: TypeVar if tp.isInstantiated => + /* `TypeMap` always strips instantiated type variables in `mapOver`. + * We can keep the original type var if its instance is not transformed + * by the LevelAvoidMap. This allows for simpler bounds and for + * derived skolems (see ApproximatingTypeMap#derivedSkolemType) to + * remain the same by keeping their info unchanged. Loosing skolems + * in the legalBound computation prevented type vars from being + * instantiated with theses skolems, even if they were within the bounds. + */ + val res = apply(tp.instanceOpt) + if res eq tp.instanceOpt then tp else res case tp: TypeParamRef => constraint.typeVarOfParam(tp) match case tvar: TypeVar => diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist index 705570f10d9c..fd40d8b3577a 100644 --- a/compiler/test/dotc/pos-test-pickling.blacklist +++ b/compiler/test/dotc/pos-test-pickling.blacklist @@ -109,4 +109,7 @@ i7445b.scala # more aggresive reduce projection makes a difference i15525.scala +i19955a.scala +i19955b.scala +i20053b.scala diff --git a/tests/pos/i19955a.scala b/tests/pos/i19955a.scala new file mode 100644 index 000000000000..b8ea95d41d24 --- /dev/null +++ b/tests/pos/i19955a.scala @@ -0,0 +1,27 @@ + +trait Summon[R, T <: R]: + type Out +object Summon: + given [R, T <: R]: Summon[R, T] with + type Out = R + +trait DFTypeAny +trait DFBits[W <: Int] extends DFTypeAny +class DFVal[+T <: DFTypeAny] +type DFValAny = DFVal[DFTypeAny] +type DFValOf[+T <: DFTypeAny] = DFVal[T] +trait Candidate[R]: + type OutW <: Int +object Candidate: + type Aux[R, O <: Int] = Candidate[R] { type OutW = O } + given [W <: Int, R <: DFValOf[DFBits[W]]]: Candidate[R] with + type OutW = W + +extension [L](lhs: L) def foo(using es: Summon[L, lhs.type]): Unit = ??? +extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW]] = ??? +extension [L <: DFValAny, W <: Int](lhs: L)(using icL: Candidate.Aux[L, W]) + def bazAux: DFValOf[DFBits[W]] = ??? + +val x = new DFVal[DFBits[4]] +val works = x.bazAux.foo +val fails = x.baz.foo \ No newline at end of file diff --git a/tests/pos/i19955b.scala b/tests/pos/i19955b.scala new file mode 100644 index 000000000000..99e101b312b1 --- /dev/null +++ b/tests/pos/i19955b.scala @@ -0,0 +1,17 @@ + +trait Wrap[W] + +trait IsWrapOfInt[R]: + type Out <: Int +given [W <: Int, R <: Wrap[W]]: IsWrapOfInt[R] with + type Out = Int + +trait IsInt[U <: Int] +given [U <: Int]: IsInt[U] = ??? + +extension [L](lhs: L) def get(using ev: IsWrapOfInt[L]): ev.Out = ??? +extension (lhs: Int) def isInt(using IsInt[lhs.type]): Unit = ??? + +val x: Wrap[Int] = ??? +val works = (x.get: Int).isInt +val fails = x.get.isInt diff --git a/tests/pos/i20053b.scala b/tests/pos/i20053b.scala new file mode 100644 index 000000000000..25180d56bbae --- /dev/null +++ b/tests/pos/i20053b.scala @@ -0,0 +1,22 @@ + +trait Sub[R, T >: R] +given [R, T >: R]: Sub[R, T] with {} + +trait Candidate[-R]: + type OutP +given [P]: Candidate[Option[P]] with + type OutP = P + +extension [L](lhs: L) + def ^^^[P](rhs: Option[P]) + (using es: Sub[lhs.type, Any]) + (using c: Candidate[L]) + (using check: c.type <:< Any): Option[c.OutP] = ??? + +val x: Option[Boolean] = ??? + +val z1 = x ^^^ x // Ok +val z2 = z1 ^^^ x // Ok +val zz = ^^^[Option[Boolean]](x ^^^ x)(x) // Ok + +val zzz = x ^^^ x ^^^ x // Error before changes From 3097d67b449b71e76c0c38f5646bee297f5cd7a4 Mon Sep 17 00:00:00 2001 From: Wojciech Mazur Date: Fri, 5 Jul 2024 18:55:42 +0200 Subject: [PATCH 2/2] Move override of mapOverTypeVar logic in ApproximatingTypeMap [Cherry-picked 6e5f540ec72a22d5f96419fcc0fd7ec7e2d30f49][modified] --- .../tools/dotc/core/ConstraintHandling.scala | 13 +------------ compiler/src/dotty/tools/dotc/core/Types.scala | 17 +++++++++++++++-- 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index c9c0db1609a7..64db5923bfea 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -240,18 +240,7 @@ trait ConstraintHandling { override def apply(tp: Type): Type = tp match case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) => legalVar(tp) - // TypeParamRef can occur in tl bounds - case tp: TypeVar if tp.isInstantiated => - /* `TypeMap` always strips instantiated type variables in `mapOver`. - * We can keep the original type var if its instance is not transformed - * by the LevelAvoidMap. This allows for simpler bounds and for - * derived skolems (see ApproximatingTypeMap#derivedSkolemType) to - * remain the same by keeping their info unchanged. Loosing skolems - * in the legalBound computation prevented type vars from being - * instantiated with theses skolems, even if they were within the bounds. - */ - val res = apply(tp.instanceOpt) - if res eq tp.instanceOpt then tp else res + // TypeParamRef can occur in tl bounds case tp: TypeParamRef => constraint.typeVarOfParam(tp) match case tvar: TypeVar => diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index fa098f6f912a..bd867c9370c0 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5760,6 +5760,10 @@ object Types extends TypeUtils { variance = saved derivedLambdaType(tp)(ptypes1, this(restpe)) + protected def mapOverTypeVar(tp: TypeVar) = + val inst = tp.instanceOpt + if (inst.exists) apply(inst) else tp + def isRange(tp: Type): Boolean = tp.isInstanceOf[Range] protected def mapCapturingType(tp: Type, parent: Type, refs: CaptureSet, v: Int): Type = @@ -5797,8 +5801,7 @@ object Types extends TypeUtils { derivedTypeBounds(tp, lo1, this(tp.hi)) case tp: TypeVar => - val inst = tp.instanceOpt - if (inst.exists) apply(inst) else tp + mapOverTypeVar(tp) case tp: ExprType => derivedExprType(tp, this(tp.resultType)) @@ -6208,6 +6211,16 @@ object Types extends TypeUtils { else super.mapCapturingType(tp, parent, refs, v) + override protected def mapOverTypeVar(tp: TypeVar) = + val inst = tp.instanceOpt + if !inst.exists then tp + else + // We can keep the original type var if its instance is not transformed + // by the ApproximatingTypeMap. This allows for simpler bounds and for + // derivedSkolemType to retain more skolems, by keeping the info unchanged. + val res = apply(inst) + if res eq inst then tp else res + protected def reapply(tp: Type): Type = apply(tp) }