Inference fails to properly use equality evidence

[kyouko-taiga]

Compiler version

3.5.0

Minimized code

Consider the following program:

trait Iter[Self]:
  type Elem
  extension (self: Self) def next: Option[(Elem, Self)]

given Iter[Int] with
  type Elem = Byte
  extension (self: Int) def next: Option[(Byte, Int)] =
    val b = self & 0xff
    if b != 0 then Some((b.toByte, self >> 8)) else None

final case class Pair[T, U](first: T, second: U)

extension[T, U](using Iter[T], T =:= U)(self: Pair[T, U])
  def hasEqualParts: Boolean =
    self.first.next match
      case None => self.second.next == None
      case Some((x, xs)) =>
        self.second.next match
          case None => false
          case Some((y, ys)) =>
            if x == y then Pair(xs, ys).hasEqualParts else false

Two errors are reported about next not being a member of U in the expressions self.second.next, revealing that the compiler failed to find next as an extension method of U, which should hold under the assumption that T is equal to U.

Perhaps more surprisingly, the following changes also result in a type error (changed lines are highlighted with //!):

extension[T, U](using Iter[T], T =:= U)(self: Pair[T, U])
  def hasEqualParts: Boolean =
    self.first.next match
      case None => self.first.next == None // !
      case Some((x, xs)) =>
        self.first.next match // !
          case None => false
          case Some((y, ys)) =>
            if x == y then Pair(xs, ys).hasEqualParts else false

The implementation is now incorrect but it should type check. Yet, the compiler complains in the last line about hasEqualParts not being a member of Pair[T, T], which is clearly not true. Note that the error disappear if:

• we remove the needless equality evidence T =:= U
• we take self as an instance of Pair[T, T]

Output

In the first example:

value next is not a member of U
value next is not a member of U

In the second example:

value hasEqualParts is not a member of Pair[T, T].
An extension method was tried, but could not be fully constructed:

    hasEqualParts[T, U](x$1, x$2)(Pair.apply[T, T](xs, ys))

    failed with:

        Found:    Pair[T, T]
        Required: Pair[T, U]

Expectation

Both version of hasEqualParts should type check.

[odersky]

I believe that's as specified. An =:= parameter between two types does not tell the Typer that the two types are equal, it will instead create implicit conversions between the two types.

And implicit conversions don't compose with extension methods. When resolving an extension method on type T, we do not allow T to be converted to something else.

So we have to use the workaround that you specified here.

I believe progress could be made but it needs quite fundamental changes. Namely, we'd have to treat implicit evidence such as =:= in the same way as GADTs. That would be a unifying scheme for GADTs and context constraints, which would require new and quite deep research.