Avoid inference getting stuck when the expected type contains a union/intersection #8635
Conversation
There was a problem hiding this comment.
Hello, and thank you for opening this PR! 🎉
All contributors have signed the CLA, thank you! ❤️
Commit Messages
We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).
Please stick to these guidelines for commit messages:
- Separate subject from body with a blank line
- When fixing an issue, start your commit message with
Fix #<ISSUE-NBR>:- Limit the subject line to 72 characters
- Capitalize the subject line
- Do not end the subject line with a period
- Use the imperative mood in the subject line ("Add" instead of "Added")
- Wrap the body at 80 characters
- Use the body to explain what and why vs. how
adapted from https://chris.beams.io/posts/git-commit
Have an awesome day! ☀️
|
Following up on the discussion of today's meeting, here's why infers To check the first goal, we try both The second goal is always true. So, the scheme is actually a lot more robust than was implied in our discussions. /cc @noti0na1 |
It turns out that this only works because of https://github.com/lampepfl/dotty/blob/8a42819bf352a25468faac3fe862d5353ea48e73/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala#L62-L63 If the parameter type of object Test {
def test1 = {
def notNull[T](x: T | Null): x.type & T = ???
val x: Int | Null = ???
val y = notNull(identity(x))
val yc: Int = y // OK
}
def test2 = {
def notNull[T](x: Any & (T | Null)): x.type & T = ???
val x: Int | Null = ???
val y = notNull(identity(x))
val yc: Int = y // FAIL
}
}The problem is that depending on how exactly the type variable of |
|
I wonder if we could get it to work reliably by making |
|
But if you check The primary reason not to check expected types that are unions is that in general that can lead to a loss |
Apparently not. The upper-bound of
Right, that's precisely the problem that this PR is fixing by using |
Hmm. That looks wrong to me. |
|
I believe it is clear that in we have to infer |
Indeed, but apparently this is intentional and cannot be avoided: https://github.com/lampepfl/dotty/blob/7a28eef2a65e769a4439aff67ff0d158db589003/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala#L480-L489
necessaryEither isn't directly related. Things break down when I remove the |
... in fact, I can work around this by wrapping the type of the parameter of notNull in an identity type lambda: type Id[A] = A
def notNull[T](x: Id[T | Null]): x.type & T = ...And then everything typechecks! I wonder if that also means we can still run into the cycles the comment above |
|
So, we have two sources of incompleteness with
This means that making use of a disjunction in the prototype risks over-approximating; that's why it is disabled. Using A way forward would if we could avoid the second form of incompleteness. That seems doable at first glance - cycle detection on the toplevel is a solvable problem. |
Yes, I just came to this conclusion too! :) And the current behavior of
Do you mean, detecting them proactively whenever we add a constraint, or reactively as we kind of already do with the deep subtype checks, etc. If the former, what would be the correct way to heal a detected cycle ? If it's a cycle like |
I mean retroactively. When adding a bound T =:= Tr & Q1 & ... & QnSo, |
…/intersection When we type a method call, we infer constraints based on its expected type before typing its arguments. This way, we can type these arguments with a precise expected type. This works fine as long as the constraints we infer based on the expected type are _necessary_ constraints, but in general type inference can go further and infer _sufficient_ constraints, meaning that we might get stuck with a set of constraints which does not allow the method arguments to be typed at all. Since 8067b95 we work around the problem by simply not propagating any constraint when the expected type is a union, but this solution is incomplete: - It only handles unions at the top-level, but the same problem can happen with unions in any covariant position (method b of or-inf.scala) as well as intersections in contravariant positions (and-inf.scala, i8378.scala) - Even when a union appear at the top-level, there might be constraints we can propagate, for example if only one branch can possibly match (method c of or-inf.scala) Thankfully, we already have a solution that works for all these problems: `TypeComparer#either` is capable of inferring only necessary constraints. So far, this was only done when inferring GADT bounds to preserve soundness, this commit extends this to use the same logic when constraining a method based on its expected type (as determined by the ConstrainResult mode). Additionally, `ConstraintHandling#addConstraint` needs to also be taught to only keep necessary constraints under this mode. Fixes scala#8378 which I previously thought was unfixable :).
|
Got everything to pass, phew! Thanks a lot for the troubleshooting help! |
| // Unlike in `TypeComparer#either`, the same reasoning does not apply | ||
| // to GADT mode because this code is never run on GADT constraints. |
There was a problem hiding this comment.
@AleksanderBG Can you confirm that this comment is correct ?
There was a problem hiding this comment.
@smarter missed your comment! GADT code only goes through addToConstraint/addUpperBound/addLowerBound. AFAIT none of these invoke addBound.
| // Unlike in `TypeComparer#either`, the same reasoning does not apply | ||
| // to GADT mode because this code is never run on GADT constraints. | ||
| if ctx.mode.is(Mode.ConstrainResult) && constraintsNarrowed then | ||
| constraint = savedConstraint |
There was a problem hiding this comment.
That looks good to me. It would be even nicer to have a prune that does not narrow. But let's save this for another day.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Given an expected type `*T`, we allow a sequence argument `xs: _*` to be either a `Seq[T]` or an `Array[_ <: T]`, irrespective of whether the method we're calling is a Java or Scala method. So far we typed sequence arguments without an expected type, meaning that adaptation did not take place. But thanks to scala#8635, we can type them with an expected type of `Seq[T] | Array[_ <: T]` and type inference works out. This is what this commit does.
Avoid inference getting stuck when the expected type contains a union/intersection
When we type a method call, we infer constraints based on its expected
type before typing its arguments. This way, we can type these arguments
with a precise expected type. This works fine as long as the constraints
we infer based on the expected type are necessary constraints, but in
general type inference can go further and infer sufficient
constraints, meaning that we might get stuck with a set of constraints
which does not allow the method arguments to be typed at all.
Since 8067b95 we work around the
problem by simply not propagating any constraint when the expected type
is a union, but this solution is incomplete:
happen with unions in any covariant position (method b of or-inf.scala)
as well as intersections in contravariant positions (and-inf.scala,
i8378.scala)
we can propagate, for example if only one branch can possibly match
(method c of or-inf.scala)
Thankfully, we already have a solution that works for all these
problems:
TypeComparer#eitheris capable of inferring only necessaryconstraints. So far, this was only done when inferring GADT bounds to
preserve soundness, this commit extends this to use the same logic when
constraining a method based on its expected type (as determined by the
ConstrainResult mode). Additionally,
ConstraintHandling#addConstraintneeds to also be taught to only keep necessary constraints under this
mode.
Fixes #8378 which I previously thought was unfixable :).