Replace GadtConstraint#isEmpty by isNarrowing

isEmpty is pointless since it is always false if we are inside  a polymorphic method.
isNarrowing computes whether the constraint actually has tigher bounds for a type variable
than the original bounds.

Author: odersky

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

@@ -43,8 +43,8 @@ sealed abstract class GadtConstraint extends Showable {
    */
   def contains(sym: Symbol)(using Context): Boolean
 
-  def isEmpty: Boolean
-  final def nonEmpty: Boolean = !isEmpty
+  /** GADT constraint narrows bounds of at least one variable */
+  def isNarrowing: Boolean
 
   /** See [[ConstraintHandling.approximation]] */
   def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type
@@ -61,13 +61,15 @@ final class ProperGadtConstraint private(
   private var myConstraint: Constraint,
   private var mapping: SimpleIdentityMap[Symbol, TypeVar],
   private var reverseMapping: SimpleIdentityMap[TypeParamRef, Symbol],
+  private var wasConstrained: Boolean
 ) extends GadtConstraint with ConstraintHandling {
   import dotty.tools.dotc.config.Printers.{gadts, gadtsConstr}
 
   def this() = this(
     myConstraint = new OrderingConstraint(SimpleIdentityMap.empty, SimpleIdentityMap.empty, SimpleIdentityMap.empty),
     mapping = SimpleIdentityMap.empty,
-    reverseMapping = SimpleIdentityMap.empty
+    reverseMapping = SimpleIdentityMap.empty,
+    wasConstrained = false
   )
 
   /** Exposes ConstraintHandling.subsumes */
@@ -149,20 +151,24 @@ final class ProperGadtConstraint private(
         if (ntTvar ne null) stripInternalTypeVar(ntTvar) else bound
       case _ => bound
     }
-    (
-      internalizedBound match {
-        case boundTvar: TypeVar =>
-          if (boundTvar eq symTvar) true
-          else if (isUpper) addLess(symTvar.origin, boundTvar.origin)
-          else addLess(boundTvar.origin, symTvar.origin)
-        case bound =>
-          addBoundTransitively(symTvar.origin, bound, isUpper)
-      }
-    ).showing({
+
+    val saved = constraint
+    val result = internalizedBound match
+      case boundTvar: TypeVar =>
+        if (boundTvar eq symTvar) true
+        else if (isUpper) addLess(symTvar.origin, boundTvar.origin)
+        else addLess(boundTvar.origin, symTvar.origin)
+      case bound =>
+        addBoundTransitively(symTvar.origin, bound, isUpper)
+
+    gadts.println {
       val descr = if (isUpper) "upper" else "lower"
       val op = if (isUpper) "<:" else ">:"
       i"adding $descr bound $sym $op $bound = $result"
-    }, gadts)
+    }
+
+    if constraint ne saved then wasConstrained = true
+    result
   }
 
   override def isLess(sym1: Symbol, sym2: Symbol)(using Context): Boolean =
@@ -193,6 +199,8 @@ final class ProperGadtConstraint private(
 
   override def contains(sym: Symbol)(using Context): Boolean = mapping(sym) ne null
 
+  def isNarrowing: Boolean = wasConstrained
+
   override def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type = {
     val res = approximation(tvarOrError(sym).origin, fromBelow = fromBelow)
     gadts.println(i"approximating $sym ~> $res")
@@ -202,19 +210,19 @@ final class ProperGadtConstraint private(
   override def fresh: GadtConstraint = new ProperGadtConstraint(
     myConstraint,
     mapping,
-    reverseMapping
+    reverseMapping,
+    wasConstrained
   )
 
   def restore(other: GadtConstraint): Unit = other match {
     case other: ProperGadtConstraint =>
       this.myConstraint = other.myConstraint
       this.mapping = other.mapping
       this.reverseMapping = other.reverseMapping
+      this.wasConstrained = other.wasConstrained
     case _ => ;
   }
 
-  override def isEmpty: Boolean = mapping.size == 0
-
   // ---- Protected/internal -----------------------------------------------
 
   override protected def constraint = myConstraint
@@ -293,7 +301,7 @@ final class ProperGadtConstraint private(
 
   override def isLess(sym1: Symbol, sym2: Symbol)(using Context): Boolean = unsupported("EmptyGadtConstraint.isLess")
 
-  override def isEmpty: Boolean = true
+  override def isNarrowing: Boolean = false
 
   override def contains(sym: Symbol)(using Context) = false
 
@@ -304,7 +312,7 @@ final class ProperGadtConstraint private(
 
   override def fresh = new ProperGadtConstraint
   override def restore(other: GadtConstraint): Unit =
-    if (!other.isEmpty) sys.error("cannot restore a non-empty GADTMap")
+    assert(!other.isNarrowing, "cannot restore a non-empty GADTMap")
 
   override def debugBoundsDescription(using Context): String = "EmptyGadtConstraint"
 

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

@@ -1662,7 +1662,7 @@ class Typer 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)
-      if ctx.gadt.nonEmpty then
+      if ctx.gadt.isNarrowing then
         // Store GADT constraint to later retrieve it (in PostTyper, for now).
         // GADT constraints are necessary to correctly check bounds of type app,
         // see tests/pos/i12226 and issue #12226. It might be possible that this
@@ -3824,7 +3824,7 @@ class Typer extends Namer
 
       pt match
         case pt: SelectionProto =>
-          if ctx.gadt.nonEmpty then
+          if ctx.gadt.isNarrowing then
             // try GADT approximation if we're trying to select a member
             // Member lookup cannot take GADTs into account b/c of cache, so we
             // approximate types based on GADT constraints instead. For an example,