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]
0

There are 0 best solutions below