Polymorphic abstract modules in Scala: projections and path-dependant types equality can't be proven

README.md

• To be short: val c: C, c.SOMETYPE value isn't equal to C#SOMETYPE. Moreover there is no any kind of relationship between them.
• dotty: scala/scala3#4583

Related:

• https://typelevel.org/blog/2015/07/19/forget-refinement-aux.html
• https://typelevel.org/blog/2015/07/13/type-members-parameters.html
• https://typelevel.org/blog/2015/07/16/method-equiv.html

full_example.scala

import scala.languageFeature.higherKinds
import scala.languageFeature.implicitConversions

trait IORunner[IO[+_]] {
  def run[T](io: IO[T]): T
}

trait Point[IO[+_]] {
  def point[T](v: T): IO[T]
}

trait Context {
  type IO[+T]


  implicit def runner: IORunner[IO]
  implicit def point: Point[IO]

  trait Aux[NIO[+_]] extends Context{
    override type IO[+T] = NIO[T]
  }

  final class IMPL[C <: Context] extends Aux[C#IO] {
    override implicit def runner: IORunner[IO] = Context.this.runner.asInstanceOf[IORunner[IO]]

    override implicit def point: Point[IO] = Context.this.point.asInstanceOf[Point[IO]]
  }

  object IMPL {
    def apply[C <: Context]: IMPL[C] = new IMPL[C]
  }
  final type DECL = this.type

  def self: IMPL[DECL] = IMPL.apply[DECL]

}

trait Super[IO[+_]] {
  def doSmth(): IO[Int]
}

class Component[C <: Context](val c: C#IMPL[C]) extends Super[C#IO] {
  import c._

  override def doSmth(): C#IO[Int] = implicitly[Point[IO]].point(1)

  def runSmth(): Int = {
    implicitly[IORunner[c.IO]].run(doSmth())
  }

}

object OptionContext extends Context {
  override type IO[+T] = Option[T]


  override implicit def point: Point[Option] = new Point[Option] {
    override def point[T](v: T): Option[T] = Option(v)
  }

  override implicit def runner: IORunner[Option] = new IORunner[Option] {
    override def run[T](io: Option[T]): T = io.get
  }

}

object App {
  def main(args: Array[String]): Unit = {
    val component = new Component(OptionContext.self)
    println(component.runSmth())
  }
}

// App.main(Array.empty) ==> 1

Problem.scala

import scala.languageFeature.higherKinds
import scala.languageFeature.implicitConversions

trait IORunner[IO[+_]] {
  def run[T](io: IO[T]): T = ???
}

trait Context {
  type IO[+T]

  implicit def runner: IORunner[IO] = ???
}

class Super[IO[+_]] {
  def doSmth(): IO[Int] = ???
}

class Component[C <: Context](val c: C) extends Super[C#IO] {
  import c._

  def x(): Int = {
    val io: C#IO[Int] = doSmth()
    // c.IO != C#IO
    implicitly[IORunner[IO]].run(io)
    implicitly[IORunner[C#IO]].run(io)
  }


}

Workaround.scala

import scala.languageFeature.higherKinds
import scala.languageFeature.implicitConversions

trait IORunner[IO[+_]] {
  def run[T](io: IO[T]): T = ???
}

trait Context {
  type IO[+T]

  implicit def runner[IO[+_]]: IORunner[IO] = ???

  trait Aux[NIO[+_]] extends Context{
    override type IO[+T] = NIO[T]
  }

  type IMPL[C <: Context] = Aux[C#IO]

}



trait Super[IO[+_]] {
  def doSmth(): IO[Int] = ???
}

class Component[C <: Context](val c: C#IMPL[C]) extends Super[C#IO] {
  import c._

  def runSmth(): Int = {
    implicitly[IORunner[c.IO]].run(doSmth())
  }

}