Check that external and internal views of inferred result types are the same

For an inferred result type, check that the type that pickled is a supertype of the
type that got inferred by capture checking. This replaces the previous checks that
the inferred type must be pure.

Author: odersky

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

@@ -1119,24 +1119,21 @@ class CheckCaptures extends Recheck, SymTransformer:
               case _ => true
             }
             if !canUseInferred then
+              // Test that the inferred type is compatible with the previously known
+              // type that other compilation units see. Compatibility means: all inferred
+              // capture sets don't contradict the externally known type, so
+              // we can use <:< instead of frozen_<:<
               val inferred = t.tpt.knownType
-              val checkPure = new TypeTraverser:
-                def traverse(tp: Type) = tp match
-                  case CapturingType(_, refs)
-                  if !refs.elems.filter(isNotPureThis).isEmpty =>// && variance >= 0 =>
-                    val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
-                    val partStr =
-                      if tp eq inferred then "with non-empty capture set"
-                      else i"since its part $tp has non-empty capture set"
-                    report.error(
-                      em"""Non-local $sym cannot have an inferred$resultStr type
-                          |$inferred
-                          |$partStr $refs.
-                          |The type needs to be declared explicitly.""".withoutDisambiguation(),
-                      t.srcPos)
-                  case _ =>
-                    traverseChildren(tp)
-              checkPure.traverse(inferred)
+              val previous = t.tpt.tpe
+              if !(inferred <:< previous) then
+                val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
+                report.error(
+                  em"""Non-local $sym cannot have an inferred$resultStr type
+                      |  $inferred
+                      |since that type does not conform to the externally known type
+                      |  $previous
+                      |The type needs to be declared explicitly.""".withoutDisambiguation(),
+                  t.srcPos)
           case t @ TypeApply(fun, args) =>
             fun.knownType.widen match
               case tl: PolyType =>

tests/neg-custom-args/captures/i15116.check

@@ -2,27 +2,31 @@
 3 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  Foo{val m: String^{Bar.this.m}}^{Bar.this.m}
-  |  with non-empty capture set {Bar.this.m}.
+  |    Foo{val m: String^{Bar.this.m}}^{Bar.this.m}
+  |  since that type does not conform to the externally known type
+  |    Foo
   |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/i15116.scala:5:6 --------------------------------------------------------------
 5 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  Foo{val m: String^}^{Baz.this}
-  |  with non-empty capture set {Baz.this}.
+  |    Foo{val m: String^}^{Baz.this}
+  |  since that type does not conform to the externally known type
+  |    Foo
   |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
 7 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  Foo{val m: String^{Bar1.this.m}}^{Bar1.this.m}
-  |  with non-empty capture set {Bar1.this.m}.
+  |    Foo{val m: String^{Bar1.this.m}}^{Bar1.this.m}
+  |  since that type does not conform to the externally known type
+  |    Foo
   |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/i15116.scala:9:6 --------------------------------------------------------------
 9 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  Foo{val m: String^}^{Baz2.this}
-  |  with non-empty capture set {Baz2.this}.
+  |    Foo{val m: String^}^{Baz2.this}
+  |  since that type does not conform to the externally known type
+  |    Foo
   |  The type needs to be declared explicitly.

tests/neg-custom-args/captures/usingLogFile.check

@@ -28,8 +28,9 @@
 47 |  val later = usingLogFile { f => () => f.write(0) } // error
    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |  Non-local value later cannot have an inferred type
-   |  () => Unit
-   |  with non-empty capture set {x$0, cap}.
+   |    () => Unit
+   |  since that type does not conform to the externally known type
+   |    () -> Unit
    |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:16 ------------------------------------------------------
 62 |    val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error