Adding full support of path-dependent GADT reasoning

[Linyxus]

Following PR #13364, this PR adds full support of path-dependent GADT reasoning. Compared to the previous one, this one will perform GADT reasoning on pattern's and scrutinee's type members, bringing richer GADT bounds.

The following shows a code snippet made possible by this PR.

type typed[E <: Expr, V] = E & { type T = V }

trait Expr { type T }
case class LitInt(x: Int) extends Expr { type T = Int }
case class Add(e1: Expr typed Int, e2: Expr typed Int) extends Expr { type T = Int }
case class LitBool(x: Boolean) extends Expr { type T = Boolean }
case class Or(e1: Expr typed Boolean, e2: Expr typed Boolean) extends Expr { type T = Boolean }

def eval(e: Expr): e.T = e match
  case LitInt(x) => x
  case Add(e1, e2) => eval(e1) + eval(e2)
  case LitBool(b) => b
  case Or(e1, e2) => eval(e1) || eval(e2)

I removed the pos test i2941 (https://github.com/lampepfl/dotty/blob/master/tests/pos/i2941.scala) because it will trigger infinite type comparison after this PR, and we investigated and found out that the problem originates from TypeComparer, but found no good solution for this issue.

[Linyxus]

Currently some tests will break. We will fix them. Let's test performance first.

[Linyxus]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit https://dotty-bench.epfl.ch/13475/ to see the changes.

Benchmarks is based on merging with master (a82a1a6)

[smarter]

This is a really cool improvement but I'm a bit concerned that we're expanding the support for GADT when there is one known GADT soundness bug: #13080, in particular is it possible that this PR could lead to this soundness bug being triggered in more situations?

[LPTK]

@smarter I don't think this risks introducing any additional injectivity problems. Indeed, working with type members eschews the whole injectivity issue – while inferring constraints from x: F[S] & F[T] requires knowledge about the injectivity of F, inferring constraints from x: { type A: S0..S1 } & { type A: T0..T1 } requires no injectivity knowledge at all.

PS: There is at least one other known GADT bug: #11545, though I suspect there are many more, due to the way GADT reasoning is currently implemented.

[anatoliykmetyuk]

This PR was left without any activity for too long and so will be closed. If you want to return to it, please feel free to reopen it and start the discussion anew.