This is both a question and a poll. Considering the following case:
trait Mat[+T]
implicitly[Mat[Product] =:= Mat[_ <: Product]]
/* Compiler error:
: Cannot prove that com.tribbloids.spike.dotty.VarianceToBoundedType.Mat[Product] =:= com.tribbloids.spike.dotty.VarianceToBoundedType.Mat[? <: Product].
*/
It is easy to prove extensionally that:
implicitly[Mat[Product] <:< Mat[_ <: Product]]
Even without the covariance decorator, As any instance of the former m: Mat[Product] can be easily proven to inhabit Mat[? <: Product]. But when covariance is introduced, the reverse should be also true. Unfortunately, both of the following statement failed:
implicitly[Mat[_ <: Product] <:< Mat[Product]]
implicitly[Mat[Product] =:= Mat[_ <: Product]]
Is this a problematic behaviour of the compiler, or I ignored some edge cases of instances that can inhabits Mat[? <: Product] but not Mat[Product]?
UPDATE 1: A derivative case looks like this:
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]
In object LessThanProductGen, the final type T is also indeterministic, The extensional equality check described above should work equally well. But the compiler reported a similar error:
: Cannot prove that ProductGen.Mat <:< LessThanProductGen.Mat
: Cannot prove that ProductGen.Mat =:= LessThanProductGen.Mat
UPDATE 2: To avoid using TGen.T as a dependent type, but as a type bound, I broke it into 2 parts, apparently this solved the problem and get my desired behaviour:
trait Mat_* {
type TT
}
trait TGen {
type T_^
type T_v <: T_^
type Mat = Mat_* { type TT <: T_^ }
// should be { type TT >: T_v <: T_^ } for invariant case
}
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]