Refactor path-dependent structural GADT reasoning

Author: Linyxus

compiler/src/dotty/tools/dotc/core/GadtConstraint.scala

@@ -62,6 +62,8 @@ sealed abstract class GadtConstraint extends Showable {
     */
   def addAllPDTsFrom(path: Type)(using Context): List[TypeRef]
 
+  def replacePath(from: Type, to: Type)(using Context): Unit
+
   /** Supplies the singleton type of the scrutinee when typechecking pattern-matches.
     */
   def withScrutinee[T](path: TermRef)(body: T): T
@@ -218,6 +220,17 @@ final class ProperGadtConstraint private(
         m.values.toList map { tv => externalize(tv.origin).asInstanceOf[TypeRef] }
     }
 
+  override def replacePath(from: Type, to: Type)(using Context): Unit =
+    val originalPairs = mapping.toList
+
+    originalPairs foreach { (tpr, tvar) =>
+      if tpr.prefix eq from then
+        val extType = TypeRef(to, tpr.symbol)
+        mapping = mapping.updated(extType, tvar)
+        mapping = mapping.remove(tpr)
+        reverseMapping = reverseMapping.updated(tvar.origin, extType)
+    }
+
   override def withScrutinee[T](path: TermRef)(body: T): T =
     val saved = this.scrutinee
     this.scrutinee = path
@@ -554,6 +567,7 @@ final class ProperGadtConstraint private(
   override def isConstrainablePDT(tp: Type)(using Context): Boolean = false
   override def addPDT(tp: Type)(using Context): Boolean = false
   override def addAllPDTsFrom(path: Type)(using Context): List[TypeRef] = null
+  override def replacePath(from: Type, to: Type)(using Context): Unit = ()
   override def withScrutinee[T](path: TermRef)(body: T): T = body
 
   override def addToConstraint(params: List[Symbol])(using Context): Boolean = unsupported("EmptyGadtConstraint.addToConstraint")

compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala

@@ -284,7 +284,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
   }
 
   /** Derive GADT bounds on type members of the scrutinee and the pattern. */
-  def constrainTypeMembers(scrut: Type, pat: Type) = trace.force(i"constraining type members $scrut >:< $pat", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") {
+  def constrainTypeMembers(scrut: Type, pat: Type, realScrutPath: TermRef, realPatPath: TermRef) = trace(i"constraining type members $scrut >:< $pat", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") {
     val saved = state.constraint
     val savedGadt = ctx.gadt.fresh
 
@@ -294,10 +294,6 @@ trait PatternTypeConstrainer { self: TypeComparer =>
     val scrutPDTs = ctx.gadt.addAllPDTsFrom(scrutPath)
     val patPDTs = ctx.gadt.addAllPDTsFrom(patPath)
 
-    println(i"scrut pdts: $scrutPDTs")
-    println(i"pat pdts: $patPDTs")
-    println(i"after adding PDTs: gadt = ${ctx.gadt.debugBoundsDescription}")
-
     val scrutSyms = Map.from {
       scrutPDTs map { pdt => pdt.symbol.name -> pdt }
     }
@@ -316,6 +312,9 @@ trait PatternTypeConstrainer { self: TypeComparer =>
     if !result then
       constraint = saved
       ctx.gadt.restore(savedGadt)
+    else
+      if realScrutPath ne null then ctx.gadt.replacePath(scrutPath, realScrutPath)
+      if realPatPath ne null then ctx.gadt.replacePath(patPath, realPatPath)
 
     result
   }

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -241,7 +241,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    *  code would have two extra parameters for each of the many calls that go from
    *  one sub-part of isSubType to another.
    */
-  protected def recur(tp1: Type, tp2: Type): Boolean = trace.force(s"isSubType ${traceInfo(tp1, tp2)}${approx.show}", subtyping) {
+  protected def recur(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)}${approx.show}", subtyping) {
 
     def monitoredIsSubType = {
       if (pendingSubTypes == null) {
@@ -2831,8 +2831,8 @@ object TypeComparer {
   def constrainPatternType(pat: Type, scrut: Type, forceInvariantRefinement: Boolean = false)(using Context): Boolean =
     comparing(_.constrainPatternType(pat, scrut, forceInvariantRefinement))
 
-  def constrainTypeMembers(scrut: Type, pat: Type)(using Context): Boolean =
-    comparing(_.constrainTypeMembers(scrut, pat))
+  def constrainTypeMembers(scrut: Type, pat: Type, scrutPath: TermRef, patPath: TermRef)(using Context): Boolean =
+    comparing(_.constrainTypeMembers(scrut, pat, scrutPath, patPath))
 
   def explained[T](op: ExplainingTypeComparer => T, header: String = "Subtype trace:")(using Context): String =
     comparing(_.explained(op, header))

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1648,17 +1648,20 @@ class Typer extends Namer
 
     val pat1 = typedPattern(tree.pat, wideSelType)(using gadtCtx)
 
-    println(i"*** typed a match case ***")
     val scrutType = sel.tpe.widen
     val patType = pat1.tpe.widen match
       case AndType(tp1, tp2) => tp2
       case tp => tp
-    println(i"scrutinee: ${scrutType} ${scrutType.toString}")
-    println(i"pat: ${patType} ${patType.toString}")
-
-    withMode(Mode.GadtConstraintInference) {
-      TypeComparer.constrainTypeMembers(scrutType, patType)(using gadtCtx)
-    }
+    val scrutPath = sel.tpe match
+      case tp: TermRef => tp
+      case _ => null
+    val patPath = pat1.tpe match
+      case tp: TermRef => tp
+      case _ => null
+
+    withMode(Mode.GadtConstraintInference)
+            (TypeComparer.constrainTypeMembers(scrutType, patType, scrutPath, patPath))
+            (using gadtCtx)
 
     caseRest(pat1)(
       using Nullables.caseContext(sel, pat1)(