-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Regression in givens #19955
Comments
I think that will have to await the improvements in the givens SIP. The second installment should handle tracked parameters. As far as I can see it only worked by accident for this very special case before. |
Why is it a special case? It's not like the problem with cascading givens, it's something different. |
If you are referring to #13580, it's not the same thing, IIUC. Notice how the given for candidate is defined. This prevents the given Out loss. |
It's simply not supported. The previous wIldcards which were allowed by accident in constraints somehow must have given the illusion that it would work, but they never were meant to solve it, nor can I see how they would be a solution. To support it, we need quite a bit of machinery, all of it implemented in the typeclasses PR. Specifically, we need to track in a class instantiation what are the precise values given as arguments. Look for tracked in the commits and discussions.
Maybe not. But the symptoms, i.e. a skolem type appearing in the error message and need for the Aux pattern to fix it, looks exactly like what tracked parameters are meant to solve. |
On a hunch I did the following trick instead of using an Aux pattern: import compiletime.ops.int.+
extension [L <: DFValAny](lhs: L)(using icL: Candidate[L]) def baz: DFValOf[DFBits[icL.OutW + 0]] = ??? This causes the code to compile successfully. |
I am not sure what it is. But the reason it worked before was that it used something that should never happen - wildcards in constraints. |
Minimisation: trait Wrap[W <: Int]
trait IsWrap[R]:
type OutW <: Int
given [W <: Int, R <: Wrap[W]]: IsWrap[R] with
type OutW = W
trait Sub[R, T >: R]
given [R, T >: R]: Sub[R, T] with {}
extension [L, W <: Int](lhs: L)(using icL: IsWrap[L]{type OutW = W}) def bazAux: Wrap[W] = ???
extension [L](lhs: L)(using icL: IsWrap[L]) def baz: Wrap[icL.OutW] = ???
extension [L](lhs: L) def foo(using es: Sub[lhs.type, L]): Unit = ???
val x: Wrap[4] = ???
val works = x.bazAux.foo
val alsoWorks =
val b = x.baz
b.foo
val fails = x.baz.foo This is the same issue as in #20053 in the case where only the third alternative is considered. Edit: further minimised to trait Wrap[W]
trait IsWrapOfInt[R]:
type Out <: Int // bound changes nothing
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 |
This also looks like the same issue as #13580 to me, it compiles by replacing the given [W <: Int, R <: DFValOf[DFBits[W]]]: Candidate[R] {type OutW = W} = ??? It seems adding |
It turns out the following assertion does not hold in the current definition of `isSameType` ```scala 3 val preConstraint = constraint val isSame = isSubType(tp1, tp2) && isSubType(tp2, tp1) isSame.ensuring(_ || constraint == preConstraint) ``` I didn't try to form a minimised snippet where this would cause a problem. But as an example, the code in #19955 (comment) produces invalid constraints which lead to suspicious looking `<notypes>`s in the subtyping trace.
by retaining instantiated type vars in LevelAvoidMap when possible. Fixes scala#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.
In scala#20120, we reach constraints with equal bounds that are intersection types, they are formed from multiple successive calls to `addOneBound`. We miss the `replace` optimization in this case because the bounds only become equal progressively, and we are only checking for equality with the constraint being added. The second tryReplace after updateEntry and isSub does not address this specific issue but scala#19955.
as an optimization In #20120, we reach constraints with equal bounds that are intersection types, they are formed from multiple successive calls to `addOneBound`. We miss the `replace` optimization in this case because the bounds only become equal progressively, and we are only checking for equality with the constraint being added. Additionally, we recheck for equal bounds after `constraint.updateEntry` as checking `isSub` can have narrowed the bounds further. #19955 is an example where this second optimization applies. Fix #20120 Close #20208 the original implementation
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]
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]
as an optimization In #20120, we reach constraints with equal bounds that are intersection types, they are formed from multiple successive calls to `addOneBound`. We miss the `replace` optimization in this case because the bounds only become equal progressively, and we are only checking for equality with the constraint being added. Additionally, we recheck for equal bounds after `constraint.updateEntry` as checking `isSub` can have narrowed the bounds further. #19955 is an example where this second optimization applies. Fix #20120 Close #20208 the original implementation [Cherry-picked c608177]
I actually first found this regression when upgrading from 3.4.0 to 3.4.1-RC1, but during minimization I reached a point where the error always surfaced until I went back to 3.0.0 and saw no error. Aux pattern can be used as a workaround. I bisected it to the versions below.
Compiler version
Last good release: 3.0.2-RC1-bin-20210609-fdbb94f-NIGHTLY
First bad release: 3.0.2-RC1-bin-20210610-fe2fcc4-NIGHTLY
bisect: ff8659e
Minimized code
Output
Expectation
No error.
The text was updated successfully, but these errors were encountered: