Adding support of path-dependent GADT reasoning

[Linyxus]

Previously, GADT reasoning only works on type parameters. This PR supports GADT reasoning for path-dependent types (that is, type members addressed from stable paths).

It mainly makes the following two things possible:

1. It allows us to utilize the GADT constraints of type members implied by the pattern matching. Example:

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  // for example: here we can derive the bound e.T = Int
  case Add(e1, e2) => eval(e1) + eval(e2)
  case LitBool(b) => b
  case Or(e1, e2) => eval(e1) || eval(e2)

2. It enables the compiler to record GADT bounds for constrainable path-dependent types even if their path is not pattern-matched against. Example:

trait Expr[+X]
case class LitInt(x: Int) extends Expr[Int]

trait TypeTag { type A }

def foo(p: TypeTag, e: Expr[p.A]): p.A = e match
  case LitInt(x) => x  // here we derive the bounds p.A >: Int, just like what we do for type parameters

Fixes #15868.

[s5bug]

What's required to push this PR to the finish line? I have a system similar to

trait T[X]
case object Foo extends T[Unit]

trait AsParam[L] {
  val tl: T[L]
}

def testParam[A](ap: AsParam[A]): Unit =
  ap.tl match {
    case Foo => println(summon[A =:= Unit])
    case _ => ()
  }

that I'd like to refactor into the equivalent of (the currently non-compiling on mainline Dotty)

trait AsMember {
  type L
  val tl: T[L]
}

def testMember(am: AsMember): Unit =
  am.tl match {
    case Foo => println(summon[am.L =:= Unit])
    case _ => ()
  }

so that methods can return AsMember instead of AsParam[?], which requires such like

val asParamQ: AsParam[?] = someFunction
asParamQ match {
  case apt: AsParam[t] => apt.tl match {
    case Foo => println(summon[t =:= Unit])
    case _ => ()
  }
}

to consume (which does happen to compile on mainline).

[Linyxus]

Hi! Glad to see this PR can benefit real-world development. It is currently blocked by #14776. This is a bug discovered when developing this PR and the tests currently broken would work after fixing this issue.

[Linyxus]

Just verified that the following snippet compiles on this branch. :)

trait T[X]
case object Foo extends T[Unit]

trait AsMember {
  type L
  val tl: T[L]
}

def testMember(am: AsMember): Unit =
  am.tl match {
    case Foo => println(summon[am.L =:= Unit])
    case _ => ()
  }

[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/14754/ to see the changes.

Benchmarks is based on merging with main (634c580)

[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/14754/ to see the changes.

Benchmarks is based on merging with main (e560c2d)

[Linyxus]

Hey Alex! @abgruszecki I have finished one round of PR polishing. I have done the following things:

• I have refactored the interface of path aliasing constraints. It is now more modular.
• I fixed the typeMemberTouched bug we discussed before, companied with a test. I also refactored the recursive calls to constrainPatternType by moving the logic into a recur function. So now we do not have typeMemberTouched argument at toplevel.
• Fixed one bug related to pattern path.
• Added tons of documentation.

There are one thing we discussed before but not in the review comments yet, so I am not sure whether I should do it: refactoring the states related to pattern and scrutinee paths into another class in Context, instead of keeping them in GadtConstraint. I am not sure what we should do here because the states for recording the scrutinee and the pattern paths are closely related to GADT reasoning and the way we implement path-dependent GADT. But maybe refactor them into another class will make things more clear and modular?

[ckipp01]

Hey @Linyxus are you willing to give this a rebase? If so, I think we can try and get this reviewed.

[Linyxus]

Similarly, we will wait for a refactorization of GADT (#15928) before proceeding this feature. I will close this for now and go back to it after the refactorization is done.

[LPTK]

#15928 was closed. Is there any future for the changes in this PR?