Backport "Improve ConstraintHandling of SkolemTypes" to LTS #21063
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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]
[Cherry-picked 6e5f540][modified]
|
No regressions detected in the community build up to lts-20227. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Backports #20175 to the LTS branch.
PR submitted by the release tooling.
[skip ci]