b: a.type but a.A != b.A

[Blaisorblade]

Even if e2: e1.type, e1.A = e2.A can still fail, in the same way, in Scala and Dotty — as of Dotty 0.16.0-bin-20190606-c46553a-NIGHTLY:
https://gist.github.com/Blaisorblade/3e5a1102c0699f05f1c11333d785a077

See castTestFail*. We need in fact e2: e1.type & something, but even then the problem doesn't always appear.
Part of the problem is triggered e2.A is aliased, because then e.A can be evaluated too eagerly; it seems Dotty tries to correct for that, but not robustly enough.

object Test {
  abstract class ExprBase { s =>
    type A
  }

  abstract class Lit extends ExprBase { s =>
    type A = Int
    val n: A
  }

  abstract class LitU extends ExprBase { s =>
    type A <: Int
    val n: A
  }

  abstract class LitL extends ExprBase { s =>
    type A <: Int
    val n: A
  }

  def castTest1(e1: ExprBase)(e2: e1.type)(x: e1.A): e2.A = x
  def castTest2(e1: ExprBase { type A = Int })(e2: e1.type)(x: e1.A): e2.A = x
  def castTest3(e1: ExprBase)(e2: ExprBase with e1.type)(x: e2.A): e1.A = x

  def castTest4(e1: ExprBase { type A = Int })(e2: ExprBase with e1.type)(x: e2.A): e1.A = x

  def castTest5a(e1: ExprBase)(e2: LitU with e1.type)(x: e2.A): e1.A = x
  def castTest5b(e1: ExprBase)(e2: LitL with e1.type)(x: e2.A): e1.A = x

  //fail:
  def castTestFail1(e1: ExprBase)(e2: Lit with e1.type)(x: e2.A): e1.A = x // this is like castTest5a/b, but with Lit instead of LitU/LitL
  // the other direction never works:
  def castTestFail2a(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = x
  def castTestFail2b(e1: ExprBase)(e2: LitL with e1.type)(x: e1.A): e2.A = x
  def castTestFail2c(e1: ExprBase)(e2: LitU with e1.type)(x: e1.A): e2.A = x

  // the problem isn't about order of intersections.
  def castTestFail2bFlip(e1: ExprBase)(e2: e1.type with LitL)(x: e1.A): e2.A = x
  def castTestFail2cFlip(e1: ExprBase)(e2: e1.type with LitU)(x: e1.A): e2.A = x

  def castTestFail3(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = {
    val y: e1.type with e2.type = e2
    val z = x: y.A
    z
  }
}

Errors

[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:31:73
[error] 31 |  def castTestFail1(e1: ExprBase)(e2: Lit with e1.type)(x: e2.A): e1.A = x // this is like castTest5a/b, but with Lit instead of LitU/LitL
[error]    |                                                                         ^
[error]    |            Found:    e2.A(x)
[error]    |            Required: e1.A'
[error]    |
[error]    |            where:    A  is a type in class Lit which is an alias of Int
[error]    |                      A' is a type in class ExprBase
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:33:74
[error] 33 |  def castTestFail2a(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = x
[error]    |                                                                          ^
[error]    |            Found:    e1.A(x)
[error]    |            Required: e2.A'
[error]    |
[error]    |            where:    A  is a type in class ExprBase
[error]    |                      A' is a type in class Lit which is an alias of Int
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:34:75
[error] 34 |  def castTestFail2b(e1: ExprBase)(e2: LitL with e1.type)(x: e1.A): e2.A = x
[error]    |                                                                           ^
[error]    |                 Found:    e1.A(x)
[error]    |                 Required: e2.A'
[error]    |
[error]    |                 where:    A  is a type in class ExprBase
[error]    |                           A' is a type in class LitL with bounds <: Int
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:35:75
[error] 35 |  def castTestFail2c(e1: ExprBase)(e2: LitU with e1.type)(x: e1.A): e2.A = x
[error]    |                                                                           ^
[error]    |                 Found:    e1.A(x)
[error]    |                 Required: e2.A'
[error]    |
[error]    |                 where:    A  is a type in class ExprBase
[error]    |                           A' is a type in class LitU with bounds <: Int
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:38:79
[error] 38 |  def castTestFail2bFlip(e1: ExprBase)(e2: e1.type with LitL)(x: e1.A): e2.A = x
[error]    |                                                                               ^
[error]    |                 Found:    e1.A(x)
[error]    |                 Required: e2.A'
[error]    |
[error]    |                 where:    A  is a type in class ExprBase
[error]    |                           A' is a type in class LitL with bounds <: Int
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:39:79
[error] 39 |  def castTestFail2cFlip(e1: ExprBase)(e2: e1.type with LitU)(x: e1.A): e2.A = x
[error]    |                                                                               ^
[error]    |                 Found:    e1.A(x)
[error]    |                 Required: e2.A'
[error]    |
[error]    |                 where:    A  is a type in class ExprBase
[error]    |                           A' is a type in class LitU with bounds <: Int
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/Papers/scala19_gadt_code/src/main/scala/openGADTs.scala:43:12
[error] 43 |    val z = x: y.A
[error]    |            ^
[error]    |            Found:    e1.A(x)
[error]    |            Required: y.A'
[error]    |
[error]    |            where:    A  is a type in class ExprBase
[error]    |                      A' is a type in class Lit which is an alias of Int
[error] 7 errors found

[abgruszecki]

To reiterate on what Paolo said, while I still understand it: the problem lies in the fact that if e.A is an alias (that is, we know that e.A === Int, for instance), TypeComparer dealiases it very early and never tries to recover from that.

If we don't know that either of e1.A or e2.A is equal to some other type (like in castTest1), the prefix comparison logic kicks in and sees that e1 and e2 are in fact the same path, therefore making the two types equal.

[Blaisorblade]

Thinking about this again, I see two algorithms. The fragile approach is trying to "undo" reduction, or catch the type before it's reduced, is unlikely to work — don't know if you could use GADT bounds for that, but @AleksanderBG would know.

What might work better: notice that e1 and e2 are aliases, and use that to reduce e1.A to Int. To notice that, you need a data structure to find aliases that find all the aliases from either representative — that's basically a union-find problem. That could also solve #6745 (tho that case maybe admits simpler solutions?).
However, I wonder where the associated data should be stored.

For performance, we should not have to explore all accessible paths: typechecking should be incomplete. That resembles subtyping relations introduced by abstract types: if L <: p.A <: U and e has type L, then e : U fails but (e : p.A) : U works. Note that, in this bug, right now no ascription can save you.

Suppose I declare somewhere a path p of type e1.type & e2.type, where e1 : A and e2 : B (and A and B might be equal or not).
Now, e1 and e2 alias each other, but finding that out would be slow: path p might be long and hidden far away, so it could be expensive to find it.

Hence, for performance, Dotty should likely not recognize eagerly that e1 and e2 alias each other.

But if I write val e1p : p.type = e1, or even e1 : p.type, then Dotty should recognize that the result aliases p, e1 and e2. An issue is that, if the union-find information is available for the whole scope, that might affect whether e1 and e2 alias each other also elsewhere — say, before the declaration of e1p. That would be very confusing.

[Blaisorblade]

BTW, https://doi.org/10.1145/3241653.3241657 describes in detail something similar to what I propose. They don't use union-find, but their data structure (path environments, a partition of paths, represented as a set of sets) gives the
right behavior (ignoring asymptotic complexity).
They alias variables too eagerly (val y = x aliases y and x, unlike in Scala), but the rest might still be relevant.

[odersky]

@Blaisorblade Nice diagnostics! See #8443 for a proposed fix.