Inconsistent success with compiling GADT pattern matching.

[TomasMikula]

First, I'm pleasantly surprised that this compiles with dotc (with scalac, it doesn't):

sealed abstract class ===[A, B]

case class Refl[A]() extends ===[A, A]

object === {

  def substitute[F[_], A, B](fa: F[A])(ev: A === B): F[B] = ev match {
    case Refl() => fa
  }

}

However, if I move the substitute method directly onto ===, it doesn't compile anymore:

sealed abstract class ===[A, B] {

  def substitute[F[_]](fa: F[A]): F[B] = this match {
    case Refl() => fa
  }

}

case class Refl[A]() extends ===[A, A]

-- [E007] Type Mismatch Error: leibniz.scala:4:19 ------------------------------
4 |    case Refl() => fa
  |                   ^^
  |                   found:    F[A](fa)
  |                   required: F[B]
  |                   
one error found

Making it an "extension" method doesn't help, either:

sealed abstract class ===[A, B]

case class Refl[A]() extends ===[A, A]

object === {

  implicit class Ops[A, B](ev: A === B) {
    def substitute[F[_]](fa: F[A]): F[B] = ev match {
      case Refl() => fa
    }
  }

}

-- [E007] Type Mismatch Error: leibniz.scala:9:21 ------------------------------
9 |      case Refl() => fa
  |                     ^^
  |                     found:    F[A](fa)
  |                     required: F[B]
  |                     
one error found

[smarter]

Duplicate of #4323, WIP PR at #4351