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.

Sign up for GitHub

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

Jump to bottom

Infer: Don't minimise to Nothing if there's an upper bound #16786

Merged
merged 1 commit into from
Jan 30, 2023
Merged

Infer: Don't minimise to Nothing if there's an upper bound #16786

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4781,7 +4781,7 @@ object Types {
def hasLowerBound(using Context): Boolean = !currentEntry.loBound.isExactlyNothing

/** For uninstantiated type variables: Is the upper bound different from Any? */
def hasUpperBound(using Context): Boolean = !currentEntry.hiBound.isRef(defn.AnyClass)
def hasUpperBound(using Context): Boolean = !currentEntry.hiBound.finalResultType.isExactlyAny
dwijnand marked this conversation as resolved.
Show resolved Hide resolved

/** Unwrap to instance (if instantiated) or origin (if not), until result
* is no longer a TypeVar
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/Inferencing.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ object Inferencing {
// else hold off instantiating unbounded unconstrained variable
else if direction != 0 then
instantiate(tvar, fromBelow = direction < 0)
else if variance >= 0 && (force.ifBottom == IfBottom.ok || tvar.hasLowerBound) then
Copy link
Contributor

@odersky odersky Aug 7, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's no motivation why the !tvar.hasUpperBound is added. It does not make sense to me. IfBottom being ok means we are allowed to minimize to Nothing. Why stop doing this if there is an upper bound?

I agree that the issue this fixes is a real one. But I am missing the reasoning why this PR is the correct fix, in particular since the PR caused regressions elsewhere.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

From the logic it seems we're happy to minimise if there's a lower bound and maximise if there's a lower bound. IfBottom, to me, looks like it's mostly for it's IfBottom.fail and IfBottom.flip alternatives - as in, IfBottom.ok is the "default"/"standard" behaviour. So under that condition, we don't want to minimise when we have an upper bound. Doing so causes the issue we're trying to fix: we have a S1 <: Pet parameter, and there are no further constraints. Consistently with everything else, it should maximise to Pet, not minimise to Nothing.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The way I read it is: If the lower bound is (missing or) Nothing then we are allowed to instantiate to the lower bound only if isBottom is OK. The upper bound has nothing to do with it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand what justifies ignoring an existing upper bound, which is exactly the i14218 case.

Copy link
Contributor

@odersky odersky Aug 7, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had a closer look at it now. Here's a slight adaptation of the original issue:

class A
class B extends A

class Z[S](v: S => Unit)
val x = new Z((s: B) => ())

x has type Z[B], as expected.

Now add a bound to S:

class Z[S <: A](v: S => Unit)

x still has type Z[B]!

But if we sharpen the bound to B:

class Z[S <: B](v: S => Unit)

then x has type Z[Nothing].

The reason this happens is because of code in Inferencing before the line in question:

            val direction = instDirection(tvar.origin)
            ...
            else if direction != 0 then
              instantiate(tvar, fromBelow = direction < 0)

The direction is set to -1 if the variable is constrained only from below and to 1 if the variable is constrained only from above. "Is constrained" means: There is a constraint stronger than the variable's bound. That's what goes wrong here: The added constrant is exactly the variable's bound, so it does not count. It's hard to change this, since the information that we also added a constraint (not just recorded the bound) is lost if the constraint is not stronger than the bound.

else if variance >= 0 && (force.ifBottom == IfBottom.ok && !tvar.hasUpperBound || tvar.hasLowerBound) then
instantiate(tvar, fromBelow = true)
else if variance >= 0 && force.ifBottom == IfBottom.fail then
return false
Expand Down
57 changes: 57 additions & 0 deletions compiler/test/dotty/tools/dotc/typer/InstantiateModel.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
package dotty.tools
package dotc
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.*

// 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

// there are 9 combinations:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I love this documentation!

// # | LB | UB | d | // d = direction
// --+----+----+---+
// 1 | L1 | AA | - | L1 <: T
// 2 | L1 | UU | - | L1 <: T <: UU
// 3 | LL | U1 | + | LL <: T <: U1
// 4 | NN | U1 | + | T <: U1
// 5 | L1 | U1 | 0 | L1 <: T <: U1
// 6 | LL | UU | 0 | LL <: T <: UU
// 7 | LL | AA | 0 | LL <: T
// 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
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
2 changes: 1 addition & 1 deletion tests/neg/i15525.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ def element22(
transmittable20.Type / transmittable21.Type
} = ???

def test22 =
def test22 = // error
Resolution(
element22(
Resolution(element0), Resolution(element0), // error // error
Expand Down
22 changes: 22 additions & 0 deletions tests/pos/i14218.http4s.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// A minimisation from http4s,
// which broke while implementing the fix for i14218.

final class Bar[+F[_]]
object Bar:
def empty[F[_]]: Bar[F] = new Bar[Nothing]

final class Foo[+F[_]]

object Foo:
def apply[F[_]](bar: Bar[F] = Bar.empty): Foo[F] = new Foo

class Test:
def test[F[_]]: Foo[F] = Foo[F]()

//-- [E007] Type Mismatch Error
//12 | def test[F[_]]: Foo[F] = Foo[F]()
// | ^^^^^^
// | Found: Bar[[_] =>> Any]
// | Required: Bar[F]
// |
// | where: F is a type in method t1 with bounds <: [_] =>> Any
15 changes: 15 additions & 0 deletions tests/pos/i14218.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
class Pet
class Cat extends Pet

class Z1[ S1 <: Pet](val fn: S1 => Unit)
class Z2[ S2 ](val fn: S2 => Unit)
class Z3[-S3 <: Pet](val fn: S3 => Unit)

abstract class Test:
def test =
val r1 = new Z1((_: Pet) => ()); eat[Z1[Pet]](r1) // the case: using the parameter bound in situ infers Z[Nothing]
val r2 = new Z2((_: Pet) => ()); eat[Z2[Pet]](r2) // counter-example: infers as desired without an upper bound
val r3 = new Z3((_: Pet) => ()); eat[Z3[Pet]](r3) // workaround: declare it contravariant
val r4 = new Z1((_: Cat) => ()); eat[Z1[Cat]](r4) // counter-example: infers as desired with a subtype

def eat[T](x: T): Unit