Type is inferred as Nothing when requiring implicit evidence =:=

[adamgfraser]

minimized code

object Example extends App {
  
  trait ZSink[-R, +E, +A0, -A, +B] {
    def flatMap[R1 <: R, E1 >: E, A00 >: A0, A1 <: A, C](
      f: B => ZSink[R1, E1, A00, A1, C]
    )(implicit ev: A00 =:= A1, e2: A1 =:= A00): ZSink[R1, E1, A00, A1, C] =
      ???
  }
  
  object ZSink {
    def identity[A]: ZSink[Any, Unit, Nothing, A, A] = ???
    def succeed[A, B](b: B): ZSink[Any, Nothing, A, A, B] = ???
  }
  
  // cannot prove that Int =:= Nothing
  ZSink.identity[Int].flatMap(n => ZSink.succeed[Int, String](n.toString))
}

expectation

I would have expected this to compile as it does on Scala 2. It appears that the issue is with the implicit evidence parameters in flatMap, since if I remove them the code compiles. In the example, succeed[Int, String] should fix both A00 and A1 to Int so I would have thought it would be straightforward to prove that A00 =:= A1 and vice versa.

Not sure if this is related to the other issues we have observed with contravariant types since one of these type parameters is contravariant. So sorry if this is redundant. We're kind of seeing the symptoms but not sure about the root causes. Thanks again for all your hard work and responsiveness and congratulations on the feature freeze!

[adamgfraser]

@odersky Thanks and happy holidays!