Skip to content

Commit

Permalink
Give up on InferExpectedTypeSuite.map/flatMap
Browse files Browse the repository at this point in the history
But keep the extraction of the instDecision logic, and keep the tests
cases I used in studying this change.

Also simplify and update InstantiateModel.  Martin had tweaked my i14218
fix to make it more conservative: in the (NN, UU) case (i.e. no inferred
bounds, only a UU upper bound declared) for covariant type parameters,
revert back to minimising to Nothing rather than maximising to the
declared bound.
  • Loading branch information
dwijnand committed Aug 21, 2024
1 parent 5aaea2f commit 43fc10c
Show file tree
Hide file tree
Showing 6 changed files with 138 additions and 56 deletions.
55 changes: 35 additions & 20 deletions compiler/src/dotty/tools/dotc/typer/Inferencing.scala
Original file line number Diff line number Diff line change
Expand Up @@ -240,25 +240,12 @@ object Inferencing {
&& {
var fail = false
var skip = false
val direction = instDirection(tvar.origin)
if minimizeSelected then
if direction <= 0 && tvar.hasLowerBound then
skip = instantiate(tvar, fromBelow = true)
else if direction >= 0 && tvar.hasUpperBound then
skip = instantiate(tvar, fromBelow = false)
// else hold off instantiating unbounded unconstrained variable
else if direction != 0 then
skip = instantiate(tvar, fromBelow = direction < 0)
else if variance >= 0 && tvar.hasLowerBound then
skip = instantiate(tvar, fromBelow = true)
else if (variance > 0 || variance == 0 && !tvar.hasUpperBound)
&& force.ifBottom == IfBottom.ok
then // if variance == 0, prefer upper bound if one is given
skip = instantiate(tvar, fromBelow = true)
else if variance >= 0 && force.ifBottom == IfBottom.fail then
fail = true
else
toMaximize = tvar :: toMaximize
instDecision(tvar, variance, minimizeSelected, force.ifBottom) match
case Decision.Min => skip = instantiate(tvar, fromBelow = true)
case Decision.Max => skip = instantiate(tvar, fromBelow = false)
case Decision.Skip => // hold off instantiating unbounded unconstrained variable
case Decision.Fail => fail = true
case Decision.ToMax => toMaximize ::= tvar
!fail && (skip || foldOver(x, tvar))
}
case tp => foldOver(x, tp)
Expand Down Expand Up @@ -452,9 +439,32 @@ object Inferencing {
if (!cmp.isSubTypeWhenFrozen(constrained.lo, original.lo)) 1 else 0
val approxAbove =
if (!cmp.isSubTypeWhenFrozen(original.hi, constrained.hi)) 1 else 0
//println(i"instDirection($param) = $approxAbove - $approxBelow original=[$original] constrained=[$constrained]")
approxAbove - approxBelow
}

/** The instantiation decision for given poly param computed from the constraint. */
enum Decision { case Min; case Max; case ToMax; case Skip; case Fail }
private def instDecision(tvar: TypeVar, v: Int, minimizeSelected: Boolean, ifBottom: IfBottom)(using Context): Decision =
import Decision.*
val direction = instDirection(tvar.origin)
val dec = if minimizeSelected then
if direction <= 0 && tvar.hasLowerBound then Min
else if direction >= 0 && tvar.hasUpperBound then Max
else Skip
else if direction != 0 then if direction < 0 then Min else Max
else if tvar.hasLowerBound then if v >= 0 then Min else ToMax
else ifBottom match
// What's left are unconstrained tvars with at most a non-Any param upperbound:
// * IfBottom.flip will always maximise to the param upperbound, for all variances
// * IfBottom.fail will fail the IFD check, for covariant or invariant tvars, maximise contravariant tvars
// * IfBottom.ok will minimise to Nothing covariant and unbounded invariant tvars, and max to Any the others
case IfBottom.ok => if v > 0 || v == 0 && !tvar.hasUpperBound then Min else ToMax // prefer upper bound if one is given
case IfBottom.fail => if v >= 0 then Fail else ToMax
case ifBottom_flip => ToMax
//println(i"instDecision($tvar, v=v, minimizedSelected=$minimizeSelected, $ifBottom) dir=$direction = $dec")
dec

/** Following type aliases and stripping refinements and annotations, if one arrives at a
* class type reference where the class has a companion module, a reference to
* that companion module. Otherwise NoType
Expand Down Expand Up @@ -651,7 +661,7 @@ trait Inferencing { this: Typer =>

val ownedVars = state.ownedVars
if (ownedVars ne locked) && !ownedVars.isEmpty then
val qualifying = ownedVars -- locked
val qualifying = (ownedVars -- locked).toList
if (!qualifying.isEmpty) {
typr.println(i"interpolate $tree: ${tree.tpe.widen} in $state, pt = $pt, owned vars = ${state.ownedVars.toList}%, %, qualifying = ${qualifying.toList}%, %, previous = ${locked.toList}%, % / ${state.constraint}")
val resultAlreadyConstrained =
Expand Down Expand Up @@ -687,6 +697,10 @@ trait Inferencing { this: Typer =>

def constraint = state.constraint

trace(i"interpolateTypeVars($tree: ${tree.tpe}, $pt, $qualifying)", typr, (_: Any) => i"$qualifying\n$constraint\n${ctx.gadt}") {
//println(i"$constraint")
//println(i"${ctx.gadt}")

/** Values of this type report type variables to instantiate with variance indication:
* +1 variable appears covariantly, can be instantiated from lower bound
* -1 variable appears contravariantly, can be instantiated from upper bound
Expand Down Expand Up @@ -804,6 +818,7 @@ trait Inferencing { this: Typer =>
end doInstantiate

doInstantiate(filterByDeps(toInstantiate))
}
}
end if
tree
Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,11 @@ import config.Printers.typr
import Inferencing.*
import ErrorReporting.*
import util.SourceFile
import util.Spans.{NoSpan, Span}
import TypeComparer.necessarySubType
import reporting.*

import scala.annotation.internal.sharable
import dotty.tools.dotc.util.Spans.{NoSpan, Span}

object ProtoTypes {

Expand Down Expand Up @@ -83,6 +84,7 @@ object ProtoTypes {
* fits the given expected result type.
*/
def constrainResult(mt: Type, pt: Type)(using Context): Boolean =
trace(i"constrainResult($mt, $pt)", typr):
val savedConstraint = ctx.typerState.constraint
val res = pt.widenExpr match {
case pt: FunProto =>
Expand Down
49 changes: 23 additions & 26 deletions compiler/test/dotty/tools/dotc/typer/InstantiateModel.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,22 +4,16 @@ package typer

// Modelling the decision in IsFullyDefined
object InstantiateModel:
enum LB { case NN; case LL; case L1 }; import LB.*
enum UB { case AA; case UU; case U1 }; import UB.*
enum Var { case V; case NotV }; import Var.*
enum MSe { case M; case NotM }; import MSe.*
enum Bot { case Fail; case Ok; case Flip }; import Bot.*
enum Act { case Min; case Max; case ToMax; case Skip; case False }; import Act.*
enum LB { case NN; case LL; case L1 }; import LB.*
enum UB { case AA; case UU; case U1 }; import UB.*
enum Decision { case Min; case Max; case ToMax; case Skip; case Fail }; import Decision.*

// NN/AA = Nothing/Any
// LL/UU = the original bounds, on the type parameter
// L1/U1 = the constrained bounds, on the type variable
// V = variance >= 0 ("non-contravariant")
// MSe = minimisedSelected
// Bot = IfBottom
// ToMax = delayed maximisation, via addition to toMaximize
// Skip = minimisedSelected "hold off instantiating"
// False = return false
// Fail = IfBottom.fail's bail option

// there are 9 combinations:
// # | LB | UB | d | // d = direction
Expand All @@ -34,24 +28,27 @@ object InstantiateModel:
// 8 | NN | UU | 0 | T <: UU
// 9 | NN | AA | 0 | T

def decide(lb: LB, ub: UB, v: Var, bot: Bot, m: MSe): Act = (lb, ub) match
def instDecision(lb: LB, ub: UB, v: Int, ifBottom: IfBottom, min: Boolean) = (lb, ub) match
case (L1, AA) => Min
case (L1, UU) => Min
case (LL, U1) => Max
case (NN, U1) => Max

case (L1, U1) => if m==M || v==V then Min else ToMax
case (LL, UU) => if m==M || v==V then Min else ToMax
case (LL, AA) => if m==M || v==V then Min else ToMax

case (NN, UU) => bot match
case _ if m==M => Max
//case Ok if v==V => Min // removed, i14218 fix
case Fail if v==V => False
case _ => ToMax

case (NN, AA) => bot match
case _ if m==M => Skip
case Ok if v==V => Min
case Fail if v==V => False
case _ => ToMax
case (L1, U1) => if min then Min else pickVar(v, Min, Min, ToMax)
case (LL, UU) => if min then Min else pickVar(v, Min, Min, ToMax)
case (LL, AA) => if min then Min else pickVar(v, Min, Min, ToMax)

case (NN, UU) => ifBottom match
case _ if min => Max
case IfBottom.ok => pickVar(v, Min, ToMax, ToMax)
case IfBottom.fail => pickVar(v, Fail, Fail, ToMax)
case IfBottom.flip => ToMax

case (NN, AA) => ifBottom match
case _ if min => Skip
case IfBottom.ok => pickVar(v, Min, Min, ToMax)
case IfBottom.fail => pickVar(v, Fail, Fail, ToMax)
case IfBottom.flip => ToMax

def pickVar[A](v: Int, cov: A, inv: A, con: A) =
if v > 0 then cov else if v == 0 then inv else con
Original file line number Diff line number Diff line change
Expand Up @@ -221,34 +221,31 @@ class InferExpectedTypeSuite extends BasePCSuite:
|""".stripMargin
)

@Ignore("Generic functions are not handled correctly.")
@Test def flatmap =
check(
"""|val _ : List[Int] = List().flatMap(_ => @@)
|""".stripMargin,
"""|IterableOnce[Int]
|""".stripMargin
"""|IterableOnce[Nothing]
|""".stripMargin // ideally IterableOnce[Int], but can't change interpolateTypeVars
)

@Ignore("Generic functions are not handled correctly.")
@Test def map =
check(
"""|val _ : List[Int] = List().map(_ => @@)
|""".stripMargin,
"""|Int
|""".stripMargin
"""|Nothing
|""".stripMargin // ideally Int, but can't change interpolateTypeVars
)

@Ignore("Generic functions are not handled correctly.")
@Test def `for-comprehension` =
check(
"""|val _ : List[Int] =
| for {
| _ <- List("a", "b")
| } yield @@
|""".stripMargin,
"""|Int
|""".stripMargin
"""|Nothing
|""".stripMargin // ideally Int, but can't change interpolateTypeVars
)

// bounds
Expand Down
12 changes: 12 additions & 0 deletions tests/pos/i21390.TrieMap.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Minimised from scala.collection.concurrent.LNode
// Useful as a minimisation of how,
// If we were to change the type interpolation
// to minimise to the inferred "X" type,
// then this is a minimisation of how the (ab)use of
// GADT constraints to handle class type params
// can fail PostTyper, -Ytest-pickler, and probably others.

import scala.language.experimental.captureChecking

class Foo[X](xs: List[X]):
def this(a: X, b: X) = this(if (a == b) then a :: Nil else a :: b :: Nil)
59 changes: 59 additions & 0 deletions tests/pos/i21390.zio.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
// A minimisation of a community build failure in PR 21390
// To see why changing the instantiation direction in interpolateTypeVars
// using the same logic as IsFullyDefined.
class Has[A]
object Has:
class Union[B, C]
object Union:
given HasHasUnion[B0 <: Has[?], C0 <: Has[?]]: Union[B0, C0] = ???

class Lay[+D]:
def and1[B1 >: D, C1](that: Lay[C1])(using Has.Union[B1, C1]): Lay[B1 & C1] = ???
def and2[B2 >: D, C2](that: Lay[C2])(using Has.Union[B2, C2]): Lay[B2 & C2] = ???

class J; type X = Has[J]
class K; type Y = Has[K]
class L; type Z = Has[L]

def t1(x: Lay[X], y: Lay[Y], z: Lay[Z]): Lay[X & Y & Z] = x.and1(y).and2(z)

/*
Here's what goes wrong in the tvar instantiation, in method t1:
1) <== constrainResult(method and1, (using x$2: Union[B1, C1]): Lay[B1 & C1], ?{ and2: ? }) = true
2) ==> Has.Union[B0, C0] <: Has.Union[B1, C1 := Y]?
3) <== Has.Union[B0, C0] <: Has.Union[B1, C1 := Y] = OK
1) B1 >: X B2 >: B1 & C1
2) B1 >: X C1 := Y B2 >: B1 & Y B0 <: Has[?] C0 <: Has[?]
3) B1 >: X <: Has[?] C1 := Y B2 >: B1 & Y B0 := B1 C0 := Y
1) Check that the result of and1 fits the expected .and2 call, inferring any necessary constraints
2) Initiate the check that calling HasHasUnion matches the needed Has.Union[B1, C1] parameter
3) In inferring that the need B0 := B1 and C0 := Y, we end up inferring B0's `<: Has[?]` on B1.
4a) <== B1.instantiate(fromBelow = true ) = X
4b) <== B1.instantiate(fromBelow = false) = Has[?]
5a) <== B2.instantiate(fromBelow = true) = X & Y
5b) <== B2.instantiate(fromBelow = true) = Y
6) <== constrainResult(method and2, (using x$2: Has.Union[B2, C2]): Lay[B2 & C2], Lay[X & Y & Z]) = true
4a) B2 >: X & Y
4b) B2 >: Y & Has[?]
5a) B2 := X & Y
5b) B2 := Y
6a) B2 >: X & Y C2 <: Z
6b) B2 >: Y C2 <: X & Z
4) With the extra upper bound constraint, we end up maximising to Has[?] (4b) instead of minimising to X (4a)
5) Which leads to instantiating B2 to just Y (5b) instead of X & Y (5a)
6) Which leads the constraints from the result of and2 to infer X & Z (6b) instead of just Z (6a)
-- [E007] Type Mismatch Error: tests/pos/i21390.zio.scala:14:73 ------------------------------------
14 |def t1(x: Lay[X], y: Lay[Y], z: Lay[Z]): Lay[X & Y & Z] = x.and1(y).and2(z)
| ^
| Found: (z : Lay[Z])
| Required: Lay[X & Z]
*/

0 comments on commit 43fc10c

Please sign in to comment.