Typeclass Instance of a Dependent Type-CodePudding

Let's say I have a Display[T] { apply(t: T): Unit } typeclass which is used in order to display instances (and I have instances for String, Int, etc.). And I also have a TCWithDependentType[T] { type DependentType ; def apply(t: T): DependentType } which transform T to TCWithDependentType#DependentType.

I'm trying to do display the instance of a DependentType, but it doesn't work because the compiler is not able to find the Display[TCWithDependentType#DependentType] (I assume it's this one) instance (even if it should be known at compile-time).

Here is the full example (associated Scastie is here: https://scastie.scala-lang.org/RXmC776DQeywLOxj2xbHQg):

trait TCWithDependentType[T]:
  type DependentType

  def apply(t: T): DependentType

def dependentTypeOf[T](t: T)(using
    tcWithDependentType: TCWithDependentType[T]
): tcWithDependentType.DependentType =
  tcWithDependentType(t)

given TCWithDependentType[Int] =
  new TCWithDependentType[Int]:
    type DependentType = String

    def apply(i: Int): String =
      s"${i}"

given TCWithDependentType[String] =
  new TCWithDependentType[String]:
    type DependentType = String

    def apply(i: String): String =
      s"${i}"

trait Display[T]:
  def apply(t: T): Unit

def display[T](t: T)(using displayForT: Display[T]): Unit =
  displayForT(t)

/* given [T]: Display[T] =
    new Display[T]:
        def apply(t: T): Unit =
            println(s"I display \"${t}\" which is unknown") */

given Display[String] =
  new Display[String]:
    def apply(t: String): Unit =
      println(s"I display \"${t}\" which is a String")

given Display[Int] =
  new Display[Int]:
    def apply(t: Int): Unit =
      println(s"I display \"${t}\" which is a Int")

val dv = dependentTypeOf(1)
display(dv)

Do you have an idea of what I'm missing in order to make this thing work?

Thanks! Adrien.

CodePudding user response：

You lost type refinements

given (TCWithDependentType[Int] {type DependentType = String}) =
  new TCWithDependentType[Int]:
    type DependentType = String
    def apply(i: Int): String = s"${i}"

given (TCWithDependentType[String] {type DependentType = String}) =
  new TCWithDependentType[String]:
    type DependentType = String
    def apply(i: String): String = s"${i}"

CodePudding user response：

You should use the standard given ... with syntax:

given TCWithDependentType[Int] with
  type DependentType = String

  def apply(i: Int): String =
    s"${i}"

That way your code looks cleaner and no type information is lost.