type equality cannot be proved with `summon[t1.X =:= t2.X]` using singleton equality of t1 and t2

[tribbloid]

Compiler version

3.6.2

Minimized code

object DependentTypeEquality {

  trait T1 {
    trait D {
      def compose(that: D): D = ???
    }

    val d: D = ???
  }

  def dummy(left: T1, right: T1)(
      using
      ev: left.type =:= right.type // singleton path equality
  ): Unit = {

    summon[left.D =:= right.D]

    left.d.compose(right.d)
  }
}

Output

/home/peng/git/dottyspike/core/src/main/scala/com/tribbloids/spike/dotty/DependentTypeEquality.scala:16:31
Cannot prove that left.D =:= right.D.
    summon[left.D =:= right.D]

/home/peng/git/dottyspike/core/src/main/scala/com/tribbloids/spike/dotty/DependentTypeEquality.scala:20:26
Found:    (right.d : right.D)
Required: left.D

Explanation
===========

Tree: right.d
I tried to show that
  (right.d : right.D)
conforms to
  left.D
but none of the attempts shown below succeeded:

  ==> (right.d : right.D)  <:  left.D CachedTermRef CachedTypeRef
    ==> right.D  <:  left.D CachedTypeRef CachedTypeRef
      ==> (right : com.tribbloids.spike.dotty.DependentTypeEquality.T1)  <:  (left : com.tribbloids.spike.dotty.DependentTypeEquality.T1) CachedTermRef CachedTermRef
        ==> com.tribbloids.spike.dotty.DependentTypeEquality.T1  <:  (left : com.tribbloids.spike.dotty.DependentTypeEquality.T1) CachedTypeRef CachedTermRef  = false

The tests were made under the empty constraint

    left.d.compose(right.d)

Expectation

since t1 and t2 are both function arguments, their most narrow types should both be path singletons, if these 2 are equal, it should imply that all their dependent types with the same symbols should also be equal.

(In addition this error message is also not sufficiently informative.)

Is =:= considered core part of the language? If not, a third-party implementation based on compile-time staging may be able to incorporate this rule while emitting more newbie-friendly error message.

[tribbloid]

if the third-party implementation is preferable, then it could even be written to be compatible with higher-kind monotonicity:

  {
    trait T2[-T] {}

    def dummy[X, Y](
        using
        ev: X <:< Y
    ): Unit = {

      summon[T2[Y] <:< T2[X]]
    }
  }

[hamzaremmal]

This works as specified and as expected. =:= and <:< don't add any information when proving other =:= and <:< relations. Similar issue in #21509.

[tribbloid]

Ah, sorry didn't see that ticket, in this case it can be merged into that.

As the professors have pointed out, a unified solver for monotonic logic would be awesome, but it takes some theoretical breakthrough