Polymorphic function type subtyping is restricted to quantifiers with equal bounds

[EugeneFlesselle]

Compiler version

3.6.0-RC1

Minimized example

val f: [A <: Int] => A => Int =
  [A <: Any] => (a: A) => 0

Output

-- [E007] Type Mismatch Error: tests/playground/example.scala:3:2 --------------
3 |  [A <: Any] => (a: A) => 0
  |  ^^^^^^^^^^^^^^^^^^^^^^^^^
  |  Found:    [A] => (a: A) => Int
  |  Required: [A <: Int] => (x$1: A) => Int

Expectation

[EugeneFlesselle]

@smarter is this an intentional restriction ?

[EugeneFlesselle]

Ah well I guess this is just a consequence of

trait F1:
  def apply[A <: Int](a: A): Int

class F2 extends F1:
  def apply[A <: Any](a: A): Int = 0

-- Error: tests/playground/example.scala:8:6 -----------------------------------
8 |class F2 extends F1:
  |      ^
  |class F2 needs to be abstract, since def apply[A <: Int](a: A): Int in trait F1 is not defined 
  |(Note that
  | parameter A in def apply[A <: Int](a: A): Int in trait F1 does not match
  | parameter A in def apply[A](a: A): Int in class F2
  | class Int in package scala is a subclass of class Any in package scala, but method parameter types must match exactly.)

😕

[smarter]

I don't recall it being an intentional restriction, the logic for methods is more restricted intentionally to avoid confusing overloads and overrides, but for polymorphic functions we don't have this constraint.

[EugeneFlesselle]

scala3/compiler/src/dotty/tools/dotc/core/TypeComparer.scala

Lines 823 to 828 in 1b644f6

	def comparePoly = tp1 match {
	case tp1: PolyType =>
	comparingTypeLambdas(tp1, tp2) {
	(tp1.signature consistentParams tp2.signature)
	&& matchingPolyParams(tp1, tp2)
	&& isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))

comparePoly requires consistentParams, but Object and Int (from the original example) are not consistent.

The following on the other hand type checks since both ParamSigs are Int:

val f: [A <: 0 | 1] => A => Int =
  [A <: Int] => (a: A) => 0 

[EugeneFlesselle]

As reminded to me by @bracevac, it is worth pointing out that full Fsub has undecidable subtyping, as opposed to kernel Fsub which requires equal bounds [TAPL-Ch.28.5].

Still we already have cases such as:

type Omega = [X[_ <: AnyKind]] =>> X[X]
type Diverge = Omega[Omega]

-- Error: tests/playground/example.scala:4:15 ----------------------------------
4 |type Diverge = Omega[Omega]
  |               ^
  |Recursion limit exceeded ...