Skip to content
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

Improve ConstraintHandling of SkolemTypes #20175

Merged
merged 2 commits into from
Apr 13, 2024

Conversation

EugeneFlesselle
Copy link
Contributor

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:

[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.

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.
@smarter
Copy link
Member

smarter commented Apr 13, 2024

This solves the issue but breaks other places which assumed the stripping of type vars in TypeMaps

Can we do it on all ApproximatingTypeMap?

@EugeneFlesselle
Copy link
Contributor Author

Can we do it on all ApproximatingTypeMap?

Doing so doesn't seem to break any thing.

@smarter smarter enabled auto-merge April 13, 2024 09:20
@smarter smarter disabled auto-merge April 13, 2024 09:21
@smarter smarter enabled auto-merge April 13, 2024 09:21
@smarter smarter disabled auto-merge April 13, 2024 09:21
@smarter smarter enabled auto-merge April 13, 2024 09:22
@smarter smarter merged commit 1ec4374 into scala:main Apr 13, 2024
16 checks passed
@smarter smarter deleted the constraint-handling/map-tvars branch April 13, 2024 10:08
@Kordyjan Kordyjan added this to the 3.5.0 milestone May 10, 2024
WojciechMazur added a commit that referenced this pull request Jul 5, 2024
Backports #20175 to the LTS branch.

PR submitted by the release tooling.
[skip ci]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Regression in givens
3 participants