scala / scala3

The Scala 3 compiler, also known as Dotty.
https://dotty.epfl.ch
Apache License 2.0
5.86k stars 1.06k forks source link

Type is incorrectly inferred as Any #7382

Open adamgfraser opened 5 years ago

adamgfraser commented 5 years ago
object Minimized {

  trait Exit[+E, +A]

  trait Fiber[+E, +A]

  trait ZIO[-R, +E, +A] {
    final def raceWith[R1 <: R, E1, E2, B, C](that: ZIO[R1, E1, B])(leftDone: (Exit[E, A], Fiber[E1, B]) => ZIO[R1, E2, C], rightDone: (Exit[E1, B], Fiber[E, A]) => ZIO[R1, E2, C]): ZIO[R1, E2, C] =
      ???
  }

  def race[R, A, B, C](left: ZIO[R, Nothing, A], right: ZIO[R, Nothing, B])(f: (Either[A, B] => C)): ZIO[R, Nothing, C] =
    left.raceWith(right)(
      (exit, right) => ???, // inferred type of right is Fiber[Any, B] rather than Fiber[Nothing, B]
      (exit, left) => ???,
    )
}

Copying @iravid.

smarter commented 5 years ago

Can you explain why Any is not what you want in this case ? From the perspective of type inference, Any is the best solution: the type of the parameter right of the lambda is Fiber[?E1, B] where ?E1 is a type variable which is not constrained, so the typechecker is free to choose any type between Nothing and Any to instantiate it. Since Fiber is covariant in its first parameter, we pick Any since that makes the lambda work with as many arguments as possible.

adamgfraser commented 5 years ago

Conceptually we are losing information. The right parameter in race has type ZIO[R, Nothing, B], which in ZIO parlance means that this effect cannot fail, and thus the fiber that results from forking it will have type Fiber[Nothing, B] and also cannot fail. In Scala 2 we could use this information to know that the lambda we provided to raceWith only had to handle the case of Fiber[Nothing, B] (i.e. it did not need to include logic for handling potential errors). In contrast, in Dotty the inferred input type to the lambda is Fiber[Any, B], indicating that the fiber could fail for any reason whatsoever and the lambda needs to contain logic for handling any possible error. Essentially, we have upcast the right parameter in race from ZIO[R, Nothing, B] to ZIO[R, Any, B], which is sound but results in the loss of all information about the error type.

In terms of type theory, I think the logic needs to be flipped because Fiber[E1, B] appears in the parameter type of the lambda and not the result type. If the expected type of the lambda is Fiber[Nothing, B] => ??? then we could provide a function Fiber[Any, B] => ???, Fiber[Unit, B] => ???, or a function that takes any other type for the error type of the fiber. In contrast, if the expected type of the lambda is Fiber[Any, B] => ??? we can only satisfy it with a function of type Fiber[Any, B] => ???. No error type other than Any will do, because we need to be able to handle any type of error.

abgruszecki commented 4 years ago

@smarter are you going to work on this?

I played around with it and while the current approach makes sense, it results in some funky behaviour:

scala> {                                                                                                                                                                                                           
     | def foo[A, B](l: List[A])(f: A => B): List[B] = l.map(f)                                                                                                                                                    
     | foo(Nil)(a => a)
     | }
def foo[A, B](l: List[A])(f: A => B): List[B]
val res2: List[Any] = List()

I would kind of expect to get a List[Nothing] out, but I get a res2: List[Any] instead.

I also tried to "lock" the type variable by using an intermediate class, but it seems that (y)our World Class Type Inference is able to defeat my scheme:

scala> class W[A](l: List[A]) extends AnyVal { def apply[B](f: A => B): List[B] = l map f }
// defined class W

scala> def bar[A](l: List[A]): W[A] = W(l)
def bar[A](l: List[A]): W[A]

scala> bar(Nil)
val res3: W[Nothing] = List()

scala> res3(a => a)
val res4: List[Nothing] = List()

scala> bar(Nil)(a => a)
val res5: List[Any] = List()

I think if we had a way to intentionally introduce type inference "boundaries", the issue code could be rewritten so that E1 = Nothing gets inferred. Do you think that makes sense?