Skip to content

Commit 6803ec6

Browse files
EugeneFlesselleWojciechMazur
authored andcommitted
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)], <empty>, <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)], <empty>, <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)], <empty>, <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)], <empty>, <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 f58cbf9]
1 parent 4fdde6b commit 6803ec6

File tree

5 files changed

+81
-1
lines changed

5 files changed

+81
-1
lines changed

Diff for: compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala

+12-1
Original file line numberDiff line numberDiff line change
@@ -240,7 +240,18 @@ trait ConstraintHandling {
240240
override def apply(tp: Type): Type = tp match
241241
case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) =>
242242
legalVar(tp)
243-
// TypeParamRef can occur in tl bounds
243+
// TypeParamRef can occur in tl bounds
244+
case tp: TypeVar if tp.isInstantiated =>
245+
/* `TypeMap` always strips instantiated type variables in `mapOver`.
246+
* We can keep the original type var if its instance is not transformed
247+
* by the LevelAvoidMap. This allows for simpler bounds and for
248+
* derived skolems (see ApproximatingTypeMap#derivedSkolemType) to
249+
* remain the same by keeping their info unchanged. Loosing skolems
250+
* in the legalBound computation prevented type vars from being
251+
* instantiated with theses skolems, even if they were within the bounds.
252+
*/
253+
val res = apply(tp.instanceOpt)
254+
if res eq tp.instanceOpt then tp else res
244255
case tp: TypeParamRef =>
245256
constraint.typeVarOfParam(tp) match
246257
case tvar: TypeVar =>

Diff for: compiler/test/dotc/pos-test-pickling.blacklist

+3
Original file line numberDiff line numberDiff line change
@@ -109,4 +109,7 @@ i7445b.scala
109109

110110
# more aggresive reduce projection makes a difference
111111
i15525.scala
112+
i19955a.scala
113+
i19955b.scala
114+
i20053b.scala
112115

Diff for: tests/pos/i19955a.scala

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
2+
trait Summon[R, T <: R]:
3+
type Out
4+
object Summon:
5+
given [R, T <: R]: Summon[R, T] with
6+
type Out = R
7+
8+
trait DFTypeAny
9+
trait DFBits[W <: Int] extends DFTypeAny
10+
class DFVal[+T <: DFTypeAny]
11+
type DFValAny = DFVal[DFTypeAny]
12+
type DFValOf[+T <: DFTypeAny] = DFVal[T]
13+
trait Candidate[R]:
14+
type OutW <: Int
15+
object Candidate:
16+
type Aux[R, O <: Int] = Candidate[R] { type OutW = O }
17+
given [W <: Int, R <: DFValOf[DFBits[W]]]: Candidate[R] with
18+
type OutW = W
19+
20+
extension [L](lhs: L) def foo(using es: Summon[L, lhs.type]): Unit = ???
21+
extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW]] = ???
22+
extension [L <: DFValAny, W <: Int](lhs: L)(using icL: Candidate.Aux[L, W])
23+
def bazAux: DFValOf[DFBits[W]] = ???
24+
25+
val x = new DFVal[DFBits[4]]
26+
val works = x.bazAux.foo
27+
val fails = x.baz.foo

Diff for: tests/pos/i19955b.scala

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
2+
trait Wrap[W]
3+
4+
trait IsWrapOfInt[R]:
5+
type Out <: Int
6+
given [W <: Int, R <: Wrap[W]]: IsWrapOfInt[R] with
7+
type Out = Int
8+
9+
trait IsInt[U <: Int]
10+
given [U <: Int]: IsInt[U] = ???
11+
12+
extension [L](lhs: L) def get(using ev: IsWrapOfInt[L]): ev.Out = ???
13+
extension (lhs: Int) def isInt(using IsInt[lhs.type]): Unit = ???
14+
15+
val x: Wrap[Int] = ???
16+
val works = (x.get: Int).isInt
17+
val fails = x.get.isInt

Diff for: tests/pos/i20053b.scala

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
2+
trait Sub[R, T >: R]
3+
given [R, T >: R]: Sub[R, T] with {}
4+
5+
trait Candidate[-R]:
6+
type OutP
7+
given [P]: Candidate[Option[P]] with
8+
type OutP = P
9+
10+
extension [L](lhs: L)
11+
def ^^^[P](rhs: Option[P])
12+
(using es: Sub[lhs.type, Any])
13+
(using c: Candidate[L])
14+
(using check: c.type <:< Any): Option[c.OutP] = ???
15+
16+
val x: Option[Boolean] = ???
17+
18+
val z1 = x ^^^ x // Ok
19+
val z2 = z1 ^^^ x // Ok
20+
val zz = ^^^[Option[Boolean]](x ^^^ x)(x) // Ok
21+
22+
val zzz = x ^^^ x ^^^ x // Error before changes

0 commit comments

Comments
 (0)