Scala's Nothing vs partial unification

Question

I would expect the following code to compile just fine:

trait Widen[M[_]] { def widen[A, B >: A](ma: M[A]): M[B] }

object Widen {
  implicit class Ops[M[_], A](ma: M[A]) {
    def widen[B >: A](implicit ev: Widen[M]): M[B] = ev.widen[A, B](ma)
  }
  // implicit class OpsNothing[M[_]](ma: M[Nothing]) {
  //   def widen[B](implicit ev: Widen[M]): M[B] = ev.widen(ma)
  // }
  implicit val WidenList = new Widen[List] { def widen[A, B >: A](l: List[A]): List[B] = l }
}

import Widen._

List.empty[Some[Int]].widen[Option[Int]]

List.empty[Nothing].widen[Int] // does not compile until uncommenting OpsNothing

But the last line does not compile. It seems to be related to partial unification because new Widen.Ops[List, Nothing](List.empty[Nothing]).widen[Int] does compile.

Now what's really weird is that if I uncomment the special case for Nothing then everything compiles.

I have no idea what's going on...

(This is using Scala 2.13.3)

Answer 1

Compiler doesn't like to infer Nothing while resolving implicits

Failed implicit resolution for Nothing with <:<

Another workaround besides OpsNothing is type Bottom

type Bottom <: Nothing
List.empty[Bottom].widen[Int] // compiles