-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Type inference issue with intersection types #8378
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
Comments
this works if Has is not invariant, is that an issue? |
Yes Has needs to be invariant. |
sorry, ignore the above |
I don't think we are looking to compose intersection types in that sense. We explicitly don't want object Example extends App {
trait Has[_]
trait A
trait B
trait C
trait ZLayer[-RIn, +E, +ROut]
object ZLayer {
def fromServices[A0, A1, B](f: (A0, A1) => B): ZLayer[Has[A0] with Has[A1], Nothing, Has[B]] =
???
}
val live: ZLayer[Has[A] & Has[B], Nothing, Has[C]] = {
val layer = ZLayer.fromServices { (a: A, b: B) =>
new C {}
}
layer
}
} Why is it that by providing additional type information in the form of an expected return type that is the actual return type that would be inferred in the absence of additional information causing this not to compile? |
ah yes, sorry, I've moderated my comment |
No worries, we're all trying to figure this out! |
I've left some comments on the corresponding scalac issues which are also applicable here: scala/bug#11898 (comment) |
@smarter Thank you! Should we close this since it doesn't sound like there is a path to addressing front he Dotty side or do you like to keep these types of issues open in case you want to come back to at some point? |
Yeah I guess I'll close since there's nothing immediately actionable here, but I'll keep this in mind. |
Also of interest: I assume you're using this weird intersection in a contravariant position to encode a union of thing, in that case you could also directly use a union in a covariant position if you were dotty-only: trait Has[A]
trait A
trait B
trait C
trait ZLayer[+RIn, +E, +ROut]
object ZLayer {
def fromServices[A0, A1, B](f: (A0, A1) => B): ZLayer[Has[A0] | Has[A1], Nothing, Has[B]] =
???
}
val live: ZLayer[Has[A] | Has[B], Nothing, Has[C]] = {
val layer = ZLayer.fromServices { (a: A, b: B) =>
new C {}
}
layer
} This infers correctly (but that's also unspecified) |
@smarter Unfortunately |
…/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. Fixes scala#8378 which I previously thought was unfixable :).
…/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. Fixes scala#8378 which I previously thought was unfixable :).
…/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. Fixes scala#8378 which I previously thought was unfixable :).
…/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. Fixes scala#8378 which I previously thought was unfixable :).
…/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 :).
I managed to find a satisfying solution, part of the latest nightly: #8635 ! :) |
minimized code
Compilation output
expectation
I would have expected this to compile because
live
expected aZLayer
with the first parameter ofHas[A] with Has[B]
, which corresponds to a function(A, B) => C
like I am providing. But the compiler seems to be expecting the first part of the intersection type twice. If I change the type signature of the first parameter in the return type offromServices
toHas[B] with Has[A]
then I get an error that the compiler expected(B, B) => C
. This issue also appears to exist on Scala 2, reported at scala/bug#11898.The text was updated successfully, but these errors were encountered: