Scala 3中协变是否应影响F[T]与F[_ <: T]的外延相等性？

从类型系统设计视角，我们需要探讨：Scala 3中，协变修饰是否应当让F[T]与F[_ <: T]具备外延相等性？

核心案例 #

定义协变特质Mat[+T]后，尝试证明Mat[Product]与Mat[_ <: Product]类型相等时，编译器报错：

trait Mat[+T]

implicitly[Mat[Product] =:= Mat[_ <: Product]]

/* 编译器错误：
Cannot prove that com.tribbloids.spike.dotty.VarianceToBoundedType.Mat[Product] =:= com.tribbloids.spike.dotty.VarianceToBoundedType.Mat[? <: Product].
*/

单向外延推导成立 #

我们可以轻松证明Mat[Product]是Mat[_ <: Product]的子类型：

implicitly[Mat[Product] <:< Mat[_ <: Product]]

即使没有协变修饰，任何Mat[Product]实例也必然属于Mat[? <: Product]的范畴。但引入协变后，反向的子类型关系及类型相等性均无法被编译器证明：

implicitly[Mat[_ <: Product] <:< Mat[Product]] // 失败
implicitly[Mat[Product] =:= Mat[_ <: Product]] // 失败

疑问 #

这是编译器的行为缺陷，还是存在某种边缘情况：有实例属于Mat[? <: Product]但不属于Mat[Product]？

更新1：衍生依赖类型案例 #

将场景转换为依赖类型定义后，同样遇到类似问题：

trait Mat_* {
  type TT
}

trait TGen {
  type T
  type Mat = Mat_* { type TT <: T }
}

object LessThanProductGen extends TGen {
  type T <: Product
}

object ProductGen extends TGen {
  final type T = Product
}

implicitly[ProductGen.Mat <:< LessThanProductGen.Mat] // 失败
implicitly[ProductGen.Mat =:= LessThanProductGen.Mat] // 失败

尽管LessThanProductGen中的T最终必然是Product的子类型，但编译器依然无法证明两者的Mat类型具备子类型关系或相等性。

更新2：拆分类型边界的解决方案 #

将TGen.T拆分为上界T_^和下界T_v后，实现了预期的类型相等性推导：

trait Mat_* {
  type TT
}

trait TGen {
  type T_^
  type T_v <: T_^
  type Mat = Mat_* { type TT <: T_^ }
  // 不变量场景下应改为 { type TT >: T_v <: T_^ }
}

object ProductGen extends TGen {
  override type T_^ = Product
  override type T_v = Product
}

object LessThanProductGen extends TGen {
  override type T_^ = Product
  override type T_v = Nothing
}

implicitly[ProductGen.Mat =:= LessThanProductGen.Mat] // 成功

内容的提问来源于stack exchange，提问作者tribbloid