Open
Description
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]
}