search

scala / scala3

The Scala 3 compiler, also known as Dotty.
https://dotty.epfl.ch
Apache License 2.0
5.84k stars 1.05k forks source link

For Covariant `F[+T]`, `F[XXX]` and `F[_ <: XXX]` should be extensionally equal #18220

Open tribbloid opened 1 year ago

tribbloid commented 1 year ago

Compiler version

3.3.0

Minimized code

      trait Mat[+T]

      summon[Mat[Product] <:< Mat[_ <: Product]]

      summon[Mat[_ <: Product] <:< Mat[Product]] // oops
      summon[Mat[Product] =:= Mat[_ <: Product]] // oops

Output

[Error] ... : Cannot prove that Mat[? <: Product] <:< Mat[Product].
[Error] ... : Cannot prove that Mat[Product] =:= Mat[? <: Product].

Expectation

(This is one of a few compiler issues that may be simplified by CoC vs λP2 conjecture)

tribbloid commented 1 year ago

the following works smoothly tho:

      trait F_* {
        type TT
      }

      trait TGen {

        type T_/\
        type T_\/ <: T_/\
        type Mat = F_* { type TT <: T_/\ }
      }

      object ProductGen extends TGen {
        override type T_/\ = Product
        override type T_\/ = Product
      }

      object LessThanProductGen extends TGen {
        override type T_/\ = Product
        override type T_\/ = Nothing

      }

      summon[ProductGen.Mat =:= LessThanProductGen.Mat]
tribbloid commented 1 year ago

The upside-down version:

Minimized code

      trait F[-T]

      summon[F[Product] <:< F[_ >: Product]]

      summon[F[_ >: Product] <:< F[Product]] // oops
      summon[F[Product] =:= F[_ >: Product]] // oops

Output

[Error] ... : Cannot prove that F[? >: Product] <:< F[Product].
[Error] ... : Cannot prove that F[Product] =:= F[? >: Product].

This works tho:

      trait F_* {
        type TT
      }

      trait TGen {

        type T_/\
        type T_\/ <: T_/\
        type F = F_* { type TT >: T_\/ }
      }

      object ProductGen extends TGen {
        override type T_/\ = Product
        override type T_\/ = Product
      }

      object MoreThanProductGen extends TGen {
        override type T_/\ = Any
        override type T_\/ = Product

      }

      summon[ProductGen.F =:= MoreThanProductGen.F]
odersky commented 1 year ago

I remove myself as assignee since I don't want to give the impression I will work on this anytime soon.