Cannot prove equivalence with a path dependent type

Question

Why does the last summon fails to compile? What can I do to make it compile?

import java.time.{LocalDateTime, LocalTime}

trait Circular[T]:
  type Parent

given localTimeCircular: Circular[LocalTime] with
  type Parent = LocalDateTime

final class CircularMap[K, +V]()(using val circular: Circular[K])

val summoned = summon[Circular[LocalTime]]
val daily = new CircularMap[LocalTime, Int]()
println(summoned == daily.circular) // Prints true

summon[localTimeCircular.Parent =:= LocalDateTime]
summon[summoned.Parent =:= LocalDateTime]

summon[daily.circular.Parent =:= LocalDateTime]

Scastie link

It fails on Scala 3.0.2 and 3.1.0-RC1

Answer 1

The thing is not in Scala 3. In Scala 2.13.6 simlar code doesn't compile

import shapeless.the

import java.time.{LocalDateTime, LocalTime}

trait Circular[T] {
  type Parent
}

implicit object localTimeCircular extends Circular[LocalTime] {
  type Parent = LocalDateTime
}
//  implicit val localTimeCircular: Circular[LocalTime] {type Parent = LocalDateTime} = new Circular[LocalTime] {
//    type Parent = LocalDateTime
//  }

final class CircularMap[K, +V]()(implicit val circular: Circular[K])

val summoned = the[Circular[LocalTime]]
val daily = new CircularMap[LocalTime, Int]()
println(summoned == daily.circular) // Prints true

implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]

//implicitly[daily.circular.Parent =:= LocalDateTime] // doesn't compile

https://scastie.scala-lang.org/DmytroMitin/lsX3fS3ET0ajzChwl2Mctw

(I replaced implicitly with the in one place because implicitly can break type refinements, summon is more like the).

Let's simplify your code in order to figure out what's going on. Let's remove implicits (let's resolve them explicitly)

import java.time.{LocalDateTime, LocalTime}

trait Circular[T] {
  type Parent
}

val localTimeCircular = new Circular[LocalTime] {
  type Parent = LocalDateTime
}

final class CircularMap[K, +V](val circular: Circular[K])

val summoned = localTimeCircular
val daily = new CircularMap[LocalTime, Int](localTimeCircular)
println(summoned == daily.circular) // Prints true

implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]

//implicitly[daily.circular.Parent =:= LocalDateTime] // doesn't compile

The thing is that path-dependent types are designed so that even if x == x1 it's not necessary that x.T =:= x1.T

In the latest release of scala (2.12.x), is the implementation of path-dependent type incomplete?

Force dependent types resolution for implicit calls

How to create an instances for typeclass with dependent type using shapeless

It's true that summoned == daily.circular but summoned has type Circular[LocalTime] { type Parent = LocalDateTime } while daily.circular has type Circular[LocalTime]. You specified it so: val circular: Circular[K]. So you upcasted refined type Circular[LocalTime] { type Parent = LocalDateTime } (let's denote it Circular.Aux[LocalTime, LocalDateTime]) to its supertype, namely the type without refinement Circular[LocalTime] (aka existential type Circular.Aux[LocalTime, _]). So types localTimeCircular.Parent and summoned.Parent are LocalDateTime but type daily.circular.Parent is abstract. If you want to restore type refinement for example you can define

final class CircularMap[K, +V, P](val circular: Circular[K] {type Parent = P})

Another way is to use singleton type

final class CircularMap[K, +V](val circular: localTimeCircular.type)

---

Is there a way to not lose the refinement Circular[LocalTime] { type Parent = LocalDateTime } without introducing the type parameter P on the class CircularMap? Something like final class CircularMap[K, +V](val circular: Circular[K] { type Parent = X }) where X would introduce a new type variable in the scope of the CircularMap body.

What you want is actually multiple type parameter lists on class (so that in class CircularMap[K, +V][P] you can specify K, V and infer P)

https://github.com/scala/bug/issues/4719

https://contributors.scala-lang.org/t/multiple-type-parameter-lists-in-dotty-si-4719/2399

You can emulate them

import java.time.{LocalDateTime, LocalTime}

trait Circular[T] {
  type Parent
}

val localTimeCircular = new Circular[LocalTime] {
  type Parent = LocalDateTime
}

trait CircularMap[K, +V] {
  type P
  val circular: Circular[K] {type Parent = P}
}
object CircularMap {
  def apply[K, V]: PartiallyApplied[K, V] = new PartiallyApplied[K, V]

  class PartiallyApplied[K, V] {
    def apply[_P](_circular: Circular[K] {type Parent = _P}): CircularMap[K, V] {type P = _P} = new CircularMap[K, V] {
      override type P = _P
      override val circular: Circular[K] {type Parent = _P} = _circular
    }
  }
}

val summoned = localTimeCircular
val daily = CircularMap[LocalTime, Int](localTimeCircular)
println(summoned == daily.circular) // Prints true

implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]
implicitly[daily.circular.Parent =:= LocalDateTime] // compiles