Error Overriding: incompatible types

[allanrenucci]

sealed abstract class <:<[-From, +To] {
  def substituteCo[F[+_]](ff: F[From]): F[To]
}

sealed abstract class =:=[From, To] extends (From <:< To) {
  override def substituteCo[F[_]](ff: F[From]): F[To] = ???
}

dotc -d out tests/allan/Test.scala
-- Error: tests/allan/Test.scala:32:15 -----------------------------------------
32 |  override def substituteCo[F[_]](ff: F[From]): F[To] = ???
   |               ^
   |error overriding method substituteCo in class <:< of type [F <: [+_$1] => Any](ff: F[From]): F[To];
   |  method substituteCo of type [F <: [_$2] => Any](ff: F[From]): F[To] has incompatible type
one error found

[smarter]

With scalac, you can override a polymorphic def with another polymorphic def with less precise bounds:

class A {
  def foo[F <: Int] = {}
}
class B extends A {
  override def foo[F] = {}
}

I think this is OK from a soundness point of view since the variance checks out, but it's kind of inconsistent with the fact that we don't allow the same for term parameters, e.g. the following doesn't work with scalac:

class A {
  def foo(x: String) = {}
}
class B extends A {
  override def foo(x: Any) = {}
}

[Blaisorblade]

I think this is OK from a soundness point of view since the variance checks out

Yes, it's just (like) contravariance of functions — I wonder if the second doesn't work just because of JVM restrictions?
Took me a second, but the "kind" of M[_] is also a "subkind" of the kind of M[+_], so the OP also checks out. No clue if/how the spec says that without kinds.

(Not that we have a soundness proof covering this contravariance, but just because we don't have a proof regarding higher-kinded types either).