In Scala 3 with DOT calculus, how to extend the equality of 2 path dependent types for obviously cases?

Question

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.

UPDATE 1 Thanks to @Mateusz I was able to determine the root cause, and it is widening type inference (a source of many complaint & SIP, e.g. https://github.com/scala/scala3/issues/3920#issuecomment-360779916)

In short, the type of v1 & v2 are Foo, not dependent at all. I have to define their types explicitly to make the compiler work:

  object Assuming {

    trait Foo {

      type S1
    }

    object Obj1 {

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

      summon[v.S1 =:= v.S1]
//      summon[Eq[v.S1, v.S1]]

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

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

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

This answered the first question, so I'm only looking for the second answer now.