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 Compound Types #11898

Open
adamgfraser opened this issue Feb 25, 2020 · 9 comments
Open

Type Inference Issue with Compound Types #11898

adamgfraser opened this issue Feb 25, 2020 · 9 comments

Comments

@adamgfraser
Copy link

@adamgfraser adamgfraser commented Feb 25, 2020

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] with Has[B], Nothing, Has[C]] =
  ZLayer.fromServices { (a: A, b: B) =>
    new C {}
  }
// type mismatch
// found:    (A, B) => C
// required: (A, A) => C
@joroKr21

This comment has been minimized.

Copy link

@joroKr21 joroKr21 commented Feb 26, 2020

That sounds like an artifact of the typechecking algorithm:

  • there is no backtracking
  • type variable constraints are accumulated during subtyping checks
  • It doesn't zip parents of refined types and try to match them somehow but it goes left to right:
    • ZLayer[Has[A0] with Has[A1], Nothing, Has[B]] <:< ZLayer[Has[A] with Has[B], Nothing, Has[C]]
    • Has[A] with Has[B] <:< Has[A0] with Has[A1]
    • Has[A] with Has[B] <:< Has[A0]
      • Has[A] <:< Has[A0] => yes A0 = A
    • Has[A] with Has[B] <:< Has[A1]
      • Has[A] <:< Has[A1] => yes A1 = A
@hrhino

This comment has been minimized.

Copy link
Member

@hrhino hrhino commented Feb 26, 2020

That sounds about right -- there's no reason that A isn't a valid instantiation for A0 and A1.

  val live: ZLayer[Has[A] with Has[B], Nothing, Has[C]] =
    ZLayer.fromServices[A, B, C] { (a, b) =>
      new C {}
    }

is only slighly more verbose (and you could kinda-curry the C type parameter if you wanted).

@adamgfraser

This comment has been minimized.

Copy link
Author

@adamgfraser adamgfraser commented Feb 26, 2020

I agree that specifying the type parameters is not that bad, but what is really strange to me is that if I use an intermediate value it also works:

  val live: ZLayer[Has[A] with Has[B], Nothing, Has[C]] = {
    val layer = ZLayer.fromServices { (a: A, b: B) =>
      new C {}
    }
    layer
  }

If I don't provide any information about the expected type it infers the return type as ZLayer[Has[A] with Has[B], Nothing, Has[C] so how does telling it the expected return type, which is the same as what would be inferred anyway, prevent it from compiling?

@joroKr21

This comment has been minimized.

Copy link

@joroKr21 joroKr21 commented Feb 26, 2020

You are still specifying the argument types explicitly and only C is inferred.

@hrhino

This comment has been minimized.

Copy link
Member

@hrhino hrhino commented Feb 26, 2020

Because Scala's being "helpful" here and trying to use the expected type (derived from the declared result type) to guide type inference, outside-in. If you have no expected type then it has to go inside-out, by typing the argument to fromServices and then seeing what that required A0 and A1 to be instantiated as.

@smarter

This comment has been minimized.

Copy link

@smarter smarter commented Feb 26, 2020

It's a combination of several things:

  1. if you have an expected type, it will be used to guide type inference
  2. Type inference then needs to get Has[A] with Has[B] <:< Has[?A0] with Has[?A1] to typecheck, and at this point there's multiple subtyping rules that can be applied that will lead to a different solution, it so happens that the implementation will choose the solution ?A0 := A; ?A1 := A
  3. When we finally try to typecheck the expression itself, we get stuck, and backtracking would be prohibitively expensive at this point.

This particular example could be fixed with some extra adhoc rules, but I don't think there's a general solution to this problem. One way forward would be to clearly specify and implement ways to guide type inference, for example using type aliases, e.g. the following works in scalac and dotty:

trait Has[A]

trait A
trait B
trait C

trait ZLayer[-RIn, +E, +ROut]

object ZLayer {
  type ZLayer2[-RIn1, -RIn2, +E, +ROut] = ZLayer[RIn1 with RIn2, E, ROut]
  def fromServices[A0, A1, B](f: (A0, A1) => B): ZLayer2[A0, A1, Nothing, Has[B]] =
    ???
}

object Test {
  val live: ZLayer.ZLayer2[A, B, Nothing, Has[C]] =
    ZLayer.fromServices { (a: A, b: B) =>
      new C {}
    }
}

It works because when checking Foo[A, B] <:< Foo[?X, ?Y], the compiler will try to match arguments before doing any decomposition, since matching arguments is the cheapest thing to try (or so I think, I didn't actually look at the logic involved here). This is currently unspecified but might be something we could formalize and enforce in the compiler.

@joroKr21

This comment has been minimized.

Copy link

@joroKr21 joroKr21 commented Feb 26, 2020

You could achieve the same effect by specifying a type alias for type |[+A, +B] = A with B and then: ZLayer[Has[A] | Has[B], Nothing, C]

But beware, it's a leaky abstraction: #10506
And in general who knows when dealiasing might occur 🤷‍♂

@smarter

This comment has been minimized.

Copy link

@smarter smarter commented Feb 26, 2020

And in general who knows when dealiasing might occur

Yeah, that's why I put the type alias at the top-level, because that ensures we'll compare the aliases first, before any dealiasing.

@adamgfraser

This comment has been minimized.

Copy link
Author

@adamgfraser adamgfraser commented Feb 26, 2020

@smarter Thank you! That is an interesting suggestion. Shall we close this issue then?

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

Successfully merging a pull request may close this issue.

None yet
4 participants
You can’t perform that action at this time.