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.

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

Type inference issue with intersection types #8378

Closed
adamgfraser opened this issue Feb 25, 2020 · 12 comments · Fixed by #8635
Closed

Type inference issue with intersection types #8378

adamgfraser opened this issue Feb 25, 2020 · 12 comments · Fixed by #8635

Comments

@adamgfraser
Copy link
Contributor

minimized code

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]] =
  ZLayer.fromServices { (a: A, b: B) =>
    new C {}
  }

Compilation output

// type mismatch
// found:    (A, B) => C
// required: (A, A) => C

expectation

I would have expected this to compile because live expected a ZLayer with the first parameter of Has[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 of fromServices to Has[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.

@bishabosha
Copy link
Member

this works if Has is not invariant, is that an issue?

@adamgfraser
Copy link
Contributor Author

Yes Has needs to be invariant.

@bishabosha
Copy link
Member

bishabosha commented Feb 25, 2020

http://dotty.epfl.ch/docs/reference/new-types/intersection-types-spec.html - according to this, intersection types only compose within a covariant constructor

sorry, ignore the above

@adamgfraser
Copy link
Contributor Author

I don't think we are looking to compose intersection types in that sense. We explicitly don't want Has[A] & Has[B] to be composed to Has[A & B]. All we want is for it to compile when we say we want Has[A] with Has[B] and we provide a value consistent with that. To highlight the strangeness here, this works fine if I use an intermediate value:

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?

@bishabosha
Copy link
Member

ah yes, sorry, I've moderated my comment

@adamgfraser
Copy link
Contributor Author

No worries, we're all trying to figure this out!

@smarter
Copy link
Member

smarter commented Feb 26, 2020

I've left some comments on the corresponding scalac issues which are also applicable here: scala/bug#11898 (comment)

@adamgfraser
Copy link
Contributor Author

@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?

@smarter
Copy link
Member

smarter commented Feb 26, 2020

Yeah I guess I'll close since there's nothing immediately actionable here, but I'll keep this in mind.

@smarter smarter closed this as completed Feb 26, 2020
@smarter
Copy link
Member

smarter commented Feb 26, 2020

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)

@neko-kai
Copy link
Contributor

neko-kai commented Feb 26, 2020

@smarter Unfortunately Has is morally covariant, it does encode an intersection, not a union – the type says you can retrieve values of A and A1 from a dynamically-typed map, but not values of any other types. It could probably be modeled without intersections in dotty, as a match type traversing a tuple of allowed keys.

smarter added a commit to dotty-staging/dotty that referenced this issue Mar 30, 2020
…/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 :).
smarter added a commit to dotty-staging/dotty that referenced this issue Mar 30, 2020
…/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 :).
smarter added a commit to dotty-staging/dotty that referenced this issue Mar 30, 2020
…/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 :).
smarter added a commit to dotty-staging/dotty that referenced this issue Apr 1, 2020
…/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 :).
smarter added a commit to dotty-staging/dotty that referenced this issue Apr 1, 2020
…/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 :).
@smarter
Copy link
Member

smarter commented Apr 3, 2020

Yeah I guess I'll close since there's nothing immediately actionable here, but I'll keep this in mind.

I managed to find a satisfying solution, part of the latest nightly: #8635 ! :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants