Considering the following example in an Object:

  object Assuming {

    trait Foo {

      type S1
    }

    object Obj1 {

      val v: Foo = ???
      val v1 = v
      val v2 = v

      implicitly[v.S1 =:= v.S1]

      // all the following failed
      implicitly[v.S1 =:= v1.S1]
      implicitly[v1.S1 =:= v2.S1]

      def fn1(v: Foo): Unit = {
        val v1 = v
        val v2 = v

        implicitly[v1.S1 =:= v2.S1]
      }
    }
  }

The 3 failures are:

[Error] E:/peng/git/dottyspike/src/main/scala/com/tribbloids/spike/dotty/DependentEquality.scala:66:33: Cannot prove that com.tribbloids.spike.dotty.DependentEquality.Assuming.Obj1.v.S1 =:= com.tribbloids.spike.dotty.DependentEquality.Assuming.Obj1.v1.S1.
[Error] E:/peng/git/dottyspike/src/main/scala/com/tribbloids/spike/dotty/DependentEquality.scala:67:34: Cannot prove that com.tribbloids.spike.dotty.DependentEquality.Assuming.Obj1.v1.S1 =:= com.tribbloids.spike.dotty.DependentEquality.Assuming.Obj1.v2.S1.
[Error] E:/peng/git/dottyspike/src/main/scala/com/tribbloids/spike/dotty/DependentEquality.scala:73:36: Cannot prove that v1.S1 =:= v2.S1.

This is obviously wrong, as v, v1, v2 obviously has the same reference within their context. In addition, the outcome won’t change if some or all of the v, v1, v2 are changed to def or lazy val.

My questions are:

• What’s the root cause of this? I know v1/v2/v have different paths, but if compiletime ops is used (https://docs.scala-lang.org/scala3/reference/metaprogramming/compiletime-ops.html), 1+1 and 2 also have different paths, yet compiler is able to resolve it successfully

• If I want to extend this behaviour, by manually introducing an assumption/axiom that v/v1/v2 are the same thing, which can work in the above cases. I would also like to carry this contextual assumption to else where, such that I can write things like:

     def fn1(v1: Foo, v2: Foo)(using v1.type =!= v2.type): Unit = {

        implicitly[v1.S1 =:= v2.S1]
     }

OR

     def fn1(v1: Foo, v2: Foo)(using Congruent[v1.type, v2.type]): Unit = {

        implicitly[v1.S1 =:= v2.S1]
     }

How do I define it? I’m OK with solution using any Scala 3 feature, but metaprogramming solutions may be accepted slower than usual