Remove GadtConstraint#remove

Pattern bound symbols infer their bounds which then get installed as
their info (in indexPattern).  So I want to remove the duplication of
info, in the persisted pickle.  However, we have a mode in TypeComparer
where we don't trust type bounds, to pessimistically protect against bad
bounds.  So removing the info from the GADT bounds made that code broke,
which is why I had looked to handling that in TypeComparer.

However, in the body of the match the pattern bound symbols can gain
more GADT bounds, so perhaps using `isPatternBound` is too naive?  And,
in general, it's a change that would need to be studied for its
soundness impact.  So, let's leave the algorithm as it is and just keep
the potential duplication.  At least for right now.

Author: dwijnand

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

@@ -50,8 +50,6 @@ sealed abstract class GadtConstraint extends Showable {
   /** See [[ConstraintHandling.approximation]] */
   def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int = Int.MaxValue)(using Context): Type
 
-  def remove(sym: Symbol)(using Context): Unit
-
   def symbols: List[Symbol]
   def inputs: List[(List[Symbol], Int)]
 
@@ -223,14 +221,6 @@ final class ProperGadtConstraint private(
     res
   }
 
-  override def remove(sym: Symbol)(using Context): Unit =
-    mapping(sym) match
-      case tv: TypeVar =>
-        mapping = mapping.remove(sym)
-        reverseMapping = reverseMapping.remove(tv.origin)
-        constraint = constraint.replace(tv.origin, sym.typeRef)
-      case null        =>
-
   override def symbols: List[Symbol] = mapping.keys
 
   override def inputs: List[(List[Symbol], Int)] =
@@ -335,8 +325,6 @@ final class ProperGadtConstraint private(
 
   override def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int)(using Context): Type = unsupported("EmptyGadtConstraint.approximation")
 
-  override def remove(sym: Symbol)(using Context): Unit = ()
-
   override def symbols: List[Symbol] = Nil
   override def inputs: List[(List[Symbol], Int)] = Nil
 

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

@@ -837,14 +837,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 isSubTypeWhenFrozen(gbounds1.hi, tp2)
                 || narrowGADTBounds(tp1, tp2, approx, isUpper = true))
 
-            def comparePatBoundInfo =
-              tp1.symbol.isPatternBound
-              && isSubTypeWhenFrozen(hi1, tp2)
-
             (!caseLambda.exists || canWidenAbstract)
                 && isSubType(hi1.boxedIfTypeParam(tp1.symbol), tp2, approx.addLow) && (trustBounds || isSubType(lo1, tp2, approx.addLow))
             || compareGADT
-            || comparePatBoundInfo
             || tryLiftedToThis1
           case _ =>
             // `Mode.RelaxedOverriding` is only enabled when checking Java overriding

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

@@ -1693,13 +1693,6 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       }
   }
 
-  private object patBindingsAcc extends TreeAccumulator[List[Symbol]] {
-    def run(tree: Tree)(using Context) = apply(Nil, tree).reverse
-    override def apply(x: List[Symbol], tree: Tree)(using Context) = tree match
-      case b: Bind if ctx.gadt.contains(b.symbol) => b.symbol :: x
-      case _ => super.foldOver(x, tree)
-  }
-
   /** If the prototype `pt` is the type lambda (when doing a dependent
    *  typing of a match), instantiate that type lambda with the pattern
    *  variables found in the pattern `pat`.
@@ -1715,10 +1708,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   /** Type a case. */
   def typedCase(tree: untpd.CaseDef, sel: Tree, wideSelType: Type, pt: Type)(using Context): CaseDef = {
     val originalCtx = ctx
-    val gadt = tree.body match
+    val previousGadt = tree.body match
       case GadtExpr(gadt, _) => gadt
-      case _                 => ctx.gadt
-    val gadtCtx: Context = ctx.fresh.setGadt(gadt.fresh).setNewScope
+      case _                 => originalCtx.gadt
+    val gadtCtx: Context = ctx.fresh.setGadt(previousGadt.fresh).setNewScope
 
     def caseRest(pat: Tree)(using Context) = {
       val pt1 = instantiateMatchTypeProto(pat, pt) match {
@@ -1728,10 +1721,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       val pat1 = indexPattern(tree).transform(pat)
       val guard1 = typedExpr(tree.guard, defn.BooleanType)
       var body1 = ensureNoLocalRefs(typedExpr(tree.body, pt1), pt1, ctx.scope.toList)
-      for sym <- patBindingsAcc.run(pat1) do ctx.gadt.remove(sym)
       if (pt1.isValueType) // insert a cast if body does not conform to expected type if we disregard gadt bounds
         body1 = body1.ensureConforms(pt1)(using originalCtx)
-      if ctx.gadt.isNarrowing && !gadt.eql(ctx.gadt) then
+      if (previousGadt ne originalCtx.gadt) || !ctx.gadt.eql(previousGadt) then
         body1 = GadtExpr(ctx.gadt, body1)
       assignType(cpy.CaseDef(tree)(pat1, guard1, body1), pat1, body1)
     }
@@ -2950,7 +2942,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
          || tree.isDef                              // ... unless tree is a definition
       then
         interpolateTypeVars(tree, pt, locked)
-        tree.overwriteType(tree.tpe.simplified)
+        tree.overwriteType(tree.tpe.simplified(using ctx.withGadt(EmptyGadtConstraint)))
     tree
 
   protected def makeContextualFunction(tree: untpd.Tree, pt: Type)(using Context): Tree = {