augment definition of `=:=` to be commutative w.r.t. implicit context

[scabug]

If you define a method that requires evidence for A =:= B, but then call some method that wants evidence for B =:= A, it will not compile, even though conceptually type equality is commutative.

It is possible to augment the definition to include a notion of commutivity, as in the following demonstration:

object commutative {
  import scala.annotation.implicitNotFound

  @implicitNotFound(msg = "Cannot prove that ${A} =::= ${B}.")
  sealed class =::=[A, B]
  object =::= {
     // type A is equal to itself
     implicit def eqAA[A]: =::=[A, A] = new =::=[A, A]

     // if B equals A, then A equals B
     implicit def eqAB[A, B](implicit eq: B =::= A): =::=[A, B] = new =::=[A, B]
  }

  // requires evidence for 'B equal A'
  def inner[A, B](implicit eqAB: B =::= A) = 0

  // requires evidence for 'A equal B'
  def outer[A, B](implicit eqAB: A =::= B) = inner[A, B]

  // compiles as desired
  val r = outer[Int, Int]

  // this fails (also as desired)
  // would like this to fail with 'implicitNotFound' message above,
  // but it fails with "diverging implicit expansion" message
  val fail = outer[Int, String]
}

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-9602?orig=1 Reporter: @erikerlandson See #4040, #5499

[scabug]

@erikerlandson said: see also: http://stackoverflow.com/questions/34404045/implicitnotfound-annotation-doesnt-apply-for-diverging-implicit-expansion

[scabug]

@retronym said: Previous attempt at this: https://github.com/scala/scala/pull/3992. Read all the way down through the comments and see https://github.com/scala/scala/commit/9f493c3840ce46d4e0646d3085bfd5c89615e6f6

In general, Scala's implicit search isn't defined for arbitrary Prolog-style solving, and trying to encode transitivity and reflexitivy rules tend to have hard to spot and harder to solve corner cases.

Related: #4040 / #5499

[scabug]

@erikerlandson said: @retronym the #3992 PR seems a lot more ambitious (and correspondingly controversial, side-effect-ful, etc) than what I'm after.

Although what I'm proposing is arguably a bit prolog-like, it seems within the bounds of standard implicit resolution logic, imo.

Far as I can tell, the addition of commutivity logic works properly, with the exception that it seems to activate a different code path on failure that doesn't honor implicitNotFound. That itself seems like a bug to me, although I'm curious about more expert opinion there.