Commits on Jul 5, 2024

1. 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]

   

   EugeneFlesselle authored and WojciechMazur committed Jul 5, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 6803ec6
   • Browse repository at this point

   Copy the full SHA

   6803ec6 View commit details

   Browse the repository at this point in the history

2. Move override of mapOverTypeVar logic in ApproximatingTypeMap …

   [Cherry-picked 6e5f540][modified]

   

   WojciechMazur committed Jul 5, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 3097d67
   • Browse repository at this point

   Copy the full SHA

   3097d67 View commit details

   Browse the repository at this point in the history