Split postcheck phase in two

Perform bounds checking before checking self types. Checking self types interpolates them,
which may give an upper approximation solution that failes subsequent bounds checks. On the
other hand, well-formedness checkimng should come after self types checking since otherwise
we get spurious "has empty capture set, cannot be tracked" messages.

Author: odersky

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -594,7 +594,9 @@ object CaptureSet:
     override def optionalInfo(using Context): String =
       for vars <- ctx.property(ShownVars) do vars += this
       val debugInfo =
-        if !isConst && ctx.settings.YccDebug.value then ids else ""
+        if !ctx.settings.YccDebug.value then ""
+        else if isConst then ids ++ "(solved)"
+        else ids
       val limitInfo =
         if ctx.settings.YprintLevel.value && level.isDefined
         then i"<at level ${level.toString}>"

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -1363,8 +1363,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       withCaptureSetsExplained:
         super.checkUnit(unit)
         checkOverrides.traverse(unit.tpdTree)
-        checkSelfTypes(unit.tpdTree)
         postCheck(unit.tpdTree)
+        checkSelfTypes(unit.tpdTree)
+        postCheckWF(unit.tpdTree)
         if ctx.settings.YccDebug.value then
           show(unit.tpdTree) // this does not print tree, but makes its variables visible for dependency printing
 
@@ -1514,7 +1515,6 @@ class CheckCaptures extends Recheck, SymTransformer:
       check.traverse(tp)
 
     /** Perform the following kinds of checks
-     *   - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
      *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
      *   - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
      */
@@ -1542,10 +1542,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           case _ =>
         end check
       end checker
-      checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
-      for chk <- todoAtPostCheck do chk()
-      setup.postCheck()
 
+      checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
       if !ctx.reporter.errorsReported then
         // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives
@@ -1557,5 +1555,15 @@ class CheckCaptures extends Recheck, SymTransformer:
             case tree: TypeTree => checkAppliedTypesIn(tree.withKnownType)
             case _ => traverseChildren(t)
         checkApplied.traverse(unit)
+    end postCheck
+
+    /** Perform the following kinds of checks:
+     *   - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
+     *   - Check that publicly visible inferred types correspond to the type
+     *     they have without capture checking.
+     */
+    def postCheckWF(unit: tpd.Tree)(using Context): Unit =
+      for chk <- todoAtPostCheck do chk()
+      setup.postCheck()
   end CaptureChecker
 end CheckCaptures

tests/pos-custom-args/captures/checkbounds.scala

@@ -0,0 +1,22 @@
+trait Dsl:
+
+    sealed trait Nat
+    case object Zero extends Nat
+    case class Succ[N <: Nat](n: N) extends Nat
+
+    type Stable[+l <: Nat, +b <: Nat, +A]
+    type Now[+l <: Nat, +b <: Nat, +A]
+    type Box[+A]
+    def stable[l <: Nat, b <: Nat, A](e: Stable[l, b, A]): Now[l, b, Box[A]]
+
+    def program[A](prog: Now[Zero.type, Zero.type, A]): Now[Zero.type, Zero.type, A]
+
+    //val conforms: Zero.type <:< Nat = summon
+    // ^ need to uncomment this line to compile with captureChecking enabled
+
+    def test: Any =
+        program[Box[Int]]:
+            val v  : Stable[Zero.type, Zero.type, Int] = ???
+            stable[Zero.type, Zero.type, Int](v)
+//          ^
+// Type argument Dsl.this.Zero.type does not conform to upper bound Dsl.this.Nat