Fix 1 cause of infinite recursion in the new provablyDisjoint.

And add an additional test for another cause of infinite recursion
that was fixed earlier.

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

@@ -2808,8 +2808,22 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
  val optGadtBounds = gadtBounds(sym)
  if optGadtBounds != null then disjointnessBoundary(optGadtBounds.hi)
  else disjointnessBoundary(tp.superTypeNormalized)
- case tp @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass =>
- tp
+ case tp @ AppliedType(tycon: TypeRef, targs) if tycon.symbol.isClass =>
+ /* The theory says we should just return `tp` here. However, due to how
+ * baseType works (called from `isBaseTypeWithDisjointArguments`),
+ * it can create infinitely growing towers of `AnnotatedType`s. This
+ * defeats the infinite recursion detection with the `pending` set.
+ * Therefore, we eagerly remove all non-refining annotations. We are
+ * allowed to do that because they don't affect subtyping (so cannot
+ * create an ill-kinded `AppliedType`) and would anyway be stripped
+ * later on by the recursive calls to `provablyDisjoint`, though
+ * `disjointnessBoundary`).
+ * See tests/pos/provably-disjoint-infinite-recursion-1.scala for an example.
+ */
+ tp.derivedAppliedType(
+ tycon,
+ targs.mapConserve(_.stripAnnots(keep = _.symbol.derivesFrom(defn.RefiningAnnotationClass)))
+ )
  case tp: TermRef =>
  val isEnumValue = tp.termSymbol.isAllOf(EnumCase, butNot = JavaDefined)
  if isEnumValue then tp

tests/pos/provably-disjoint-infinite-recursion-1.scala

@@ -0,0 +1,4 @@
+class Test {
+ def isTraversableAgain(from: Iterator[Int]): Boolean =
+ from.isInstanceOf[Iterable[?]]
+}

tests/pos/provably-disjoint-infinite-recursion-2.scala

@@ -0,0 +1,10 @@
+type Tupled[A] <: Tuple = A match
+ case Tuple => A & Tuple
+ case _ => A *: EmptyTuple
+
+enum Day:
+ case Saturday, Sunday
+
+type Foo = Tupled[Day]
+
+def foo(): Foo = Day.Saturday *: EmptyTuple