Shorten traces for TypeMismatch errors under -explain (scala#18742)

This is a partial fix for scala#18737. We still can't explain the differences concisely, but at least we shorten the comparison traces by showing only steps that contributed to the overall failure and by avoiding repetitions.
dotty-staging · Oct 25, 2023 · 38559d7 · 38559d7
2 parents 15033c7 + afa2e30
commit 38559d7
Show file tree

Hide file tree

Showing 7 changed files with 130 additions and 53 deletions.
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -253,7 +253,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         //}
         assert(!ctx.settings.YnoDeepSubtypes.value)
         if (Config.traceDeepSubTypeRecursions && !this.isInstanceOf[ExplainingTypeComparer])
-          report.log(explained(_.isSubType(tp1, tp2, approx)))
+          report.log(explained(_.isSubType(tp1, tp2, approx), short = false))
       }
       // Eliminate LazyRefs before checking whether we have seen a type before
       val normalize = new TypeMap with CaptureSet.IdempotentCaptRefMap {
@@ -2959,7 +2959,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     }
   }
 
-  protected def explainingTypeComparer = ExplainingTypeComparer(comparerContext)
+  protected def explainingTypeComparer(short: Boolean) = ExplainingTypeComparer(comparerContext, short)
   protected def trackingTypeComparer = TrackingTypeComparer(comparerContext)
 
   private def inSubComparer[T, Cmp <: TypeComparer](comparer: Cmp)(op: Cmp => T): T =
@@ -2969,8 +2969,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     finally myInstance = saved
 
   /** The trace of comparison operations when performing `op` */
-  def explained[T](op: ExplainingTypeComparer => T, header: String = "Subtype trace:")(using Context): String =
-    val cmp = explainingTypeComparer
+  def explained[T](op: ExplainingTypeComparer => T, header: String = "Subtype trace:", short: Boolean)(using Context): String =
+    val cmp = explainingTypeComparer(short)
     inSubComparer(cmp)(op)
     cmp.lastTrace(header)
 
@@ -3139,8 +3139,8 @@ object TypeComparer {
   def constrainPatternType(pat: Type, scrut: Type, forceInvariantRefinement: Boolean = false)(using Context): Boolean =
     comparing(_.constrainPatternType(pat, scrut, forceInvariantRefinement))
 
-  def explained[T](op: ExplainingTypeComparer => T, header: String = "Subtype trace:")(using Context): String =
-    comparing(_.explained(op, header))
+  def explained[T](op: ExplainingTypeComparer => T, header: String = "Subtype trace:", short: Boolean = false)(using Context): String =
+    comparing(_.explained(op, header, short))
 
   def tracked[T](op: TrackingTypeComparer => T)(using Context): T =
     comparing(_.tracked(op))
@@ -3337,30 +3337,47 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   }
 }
 
-/** A type comparer that can record traces of subtype operations */
-class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
+/** A type comparer that can record traces of subtype operations
+ *  @param short  if true print only failing forward traces; never print succesful
+ *                subtraces; never print backtraces starting with `<==`.
+ */
+class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeComparer(initctx) {
   import TypeComparer._
 
   init(initctx)
 
-  override def explainingTypeComparer = this
+  override def explainingTypeComparer(short: Boolean) =
+    if short == this.short then this
+    else ExplainingTypeComparer(comparerContext, short)
 
   private var indent = 0
   private val b = new StringBuilder
-
-  private var skipped = false
+  private var lastForwardGoal: String | Null = null
 
   override def traceIndented[T](str: String)(op: => T): T =
-    if (skipped) op
-    else {
+    val str1 = str.replace('\n', ' ')
+    if short && str1 == lastForwardGoal then
+      op // repeated goal, skip for clarity
+    else
+      lastForwardGoal = str1
+      val curLength = b.length
       indent += 2
-      val str1 = str.replace('\n', ' ')
       b.append("\n").append(" " * indent).append("==> ").append(str1)
       val res = op
-      b.append("\n").append(" " * indent).append("<== ").append(str1).append(" = ").append(show(res))
+      if short then
+        if res == false then
+          if lastForwardGoal != null then  // last was deepest goal that failed
+            b.append("  = false")
+            lastForwardGoal = null
+        else
+          b.length = curLength // don't show successful subtraces
+      else
+        b.append("\n").append(" " * indent).append("<== ").append(str1).append(" = ").append(show(res))
       indent -= 2
       res
-    }
+
+  private def traceIndentedIfNotShort[T](str: String)(op: => T): T =
+    if short then op else traceIndented(str)(op)
 
   private def frozenNotice: String =
     if frozenConstraint then " in frozen constraint" else ""
@@ -3371,7 +3388,8 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       then s" ${tp1.getClass} ${tp2.getClass}"
       else ""
     val approx = approxState
-    traceIndented(s"${show(tp1)}  <:  ${show(tp2)}$moreInfo${approx.show}$frozenNotice") {
+    def approxStr = if short then "" else approx.show
+    traceIndented(s"${show(tp1)}  <:  ${show(tp2)}$moreInfo${approxStr}$frozenNotice") {
       super.recur(tp1, tp2)
     }
 
@@ -3381,12 +3399,12 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
     }
 
   override def lub(tp1: Type, tp2: Type, canConstrain: Boolean, isSoft: Boolean): Type =
-    traceIndented(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain, isSoft=$isSoft)") {
+    traceIndentedIfNotShort(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain, isSoft=$isSoft)") {
       super.lub(tp1, tp2, canConstrain, isSoft)
     }
 
   override def glb(tp1: Type, tp2: Type): Type =
-    traceIndented(s"glb(${show(tp1)}, ${show(tp2)})") {
+    traceIndentedIfNotShort(s"glb(${show(tp1)}, ${show(tp2)})") {
       super.glb(tp1, tp2)
     }
 

diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -204,7 +204,7 @@ object ErrorReporting {
           |  $found
           |conforms to
           |  $expected
-          |but the comparison trace ended with `false`:
+          |but none of the attempts shown below succeeded:
           |"""
       val c = ctx.typerState.constraint
       val constraintText =
@@ -213,7 +213,7 @@ object ErrorReporting {
         else
           i"""a constraint with:
              |$c"""
-      i"""${TypeComparer.explained(_.isSubType(found, expected), header)}
+      i"""${TypeComparer.explained(_.isSubType(found, expected), header, short = !ctx.settings.Ydebug.value)}
          |
          |The tests were made under $constraintText"""
 

diff --git a/tests/neg/hidden-type-errors.check b/tests/neg/hidden-type-errors.check
@@ -12,12 +12,9 @@
   |   String
   | conforms to
   |   Int
-  | but the comparison trace ended with `false`:
+  | but none of the attempts shown below succeeded:
   |
-  |   ==> String  <:  Int
-  |     ==> String  <:  Int
-  |     <== String  <:  Int = false
-  |   <== String  <:  Int = false
+  |   ==> String  <:  Int  = false
   |
   | The tests were made under the empty constraint
    ---------------------------------------------------------------------------------------------------------------------
diff --git a/tests/neg/i11637.check b/tests/neg/i11637.check
@@ -9,20 +9,13 @@
    |   test2.FunctorImpl
    | conforms to
    |   [Generic2[T <: String] <: Set[T]] =>> Any
-   | but the comparison trace ended with `false`:
+   | but none of the attempts shown below succeeded:
    |
    |   ==> test2.FunctorImpl  <:  [Generic2[T <: String] <: Set[T]] =>> Any
    |     ==> type bounds [[T <: String] <: Set[T]]  <:  type bounds [[T] <: Iterable[T]]
    |       ==> [T <: String] =>> Set[T]  <:  Iterable
    |         ==> type bounds []  <:  type bounds [ <: String]
-   |           ==> Any  <:  String
-   |             ==> Any  <:  String
-   |             <== Any  <:  String = false
-   |           <== Any  <:  String = false
-   |         <== type bounds []  <:  type bounds [ <: String] = false
-   |       <== [T <: String] =>> Set[T]  <:  Iterable = false
-   |     <== type bounds [[T <: String] <: Set[T]]  <:  type bounds [[T] <: Iterable[T]] = false
-   |   <== test2.FunctorImpl  <:  [Generic2[T <: String] <: Set[T]] =>> Any = false
+   |           ==> Any  <:  String  = false
    |
    | The tests were made under the empty constraint
     --------------------------------------------------------------------------------------------------------------------
@@ -37,20 +30,13 @@
    |   test2.FunctorImpl
    | conforms to
    |   [Generic2[T <: String] <: Set[T]] =>> Any
-   | but the comparison trace ended with `false`:
+   | but none of the attempts shown below succeeded:
    |
    |   ==> test2.FunctorImpl  <:  [Generic2[T <: String] <: Set[T]] =>> Any
    |     ==> type bounds [[T <: String] <: Set[T]]  <:  type bounds [[T] <: Iterable[T]]
    |       ==> [T <: String] =>> Set[T]  <:  Iterable
    |         ==> type bounds []  <:  type bounds [ <: String]
-   |           ==> Any  <:  String
-   |             ==> Any  <:  String
-   |             <== Any  <:  String = false
-   |           <== Any  <:  String = false
-   |         <== type bounds []  <:  type bounds [ <: String] = false
-   |       <== [T <: String] =>> Set[T]  <:  Iterable = false
-   |     <== type bounds [[T <: String] <: Set[T]]  <:  type bounds [[T] <: Iterable[T]] = false
-   |   <== test2.FunctorImpl  <:  [Generic2[T <: String] <: Set[T]] =>> Any = false
+   |           ==> Any  <:  String  = false
    |
    | The tests were made under the empty constraint
     --------------------------------------------------------------------------------------------------------------------
diff --git a/tests/neg/i15575.check b/tests/neg/i15575.check
@@ -9,12 +9,10 @@
   |   Any
   | conforms to
   |   T & Any
-  | but the comparison trace ended with `false`:
+  | but none of the attempts shown below succeeded:
   |
   |   ==> Any  <:  T & Any
-  |     ==> Any  <:  T
-  |     <== Any  <:  T = false
-  |   <== Any  <:  T & Any = false
+  |     ==> Any  <:  T  = false
   |
   | The tests were made under the empty constraint
    ---------------------------------------------------------------------------------------------------------------------
@@ -29,12 +27,9 @@
   |   CharSequence
   | conforms to
   |   String
-  | but the comparison trace ended with `false`:
+  | but none of the attempts shown below succeeded:
   |
-  |   ==> CharSequence  <:  String
-  |     ==> CharSequence  <:  String
-  |     <== CharSequence  <:  String = false
-  |   <== CharSequence  <:  String = false
+  |   ==> CharSequence  <:  String  = false
   |
   | The tests were made under the empty constraint
    ---------------------------------------------------------------------------------------------------------------------
diff --git a/tests/neg/i18737.check b/tests/neg/i18737.check
@@ -0,0 +1,75 @@
+-- [E007] Type Mismatch Error: tests/neg/i18737.scala:3:36 -------------------------------------------------------------
+3 |def test2(v: String & Long) = test1(v)  // error
+  |                                    ^
+  |                                    Found:    (v : String & Long)
+  |                                    Required: String & Integer & List[String]
+  |---------------------------------------------------------------------------------------------------------------------
+  | Explanation (enabled by `-explain`)
+  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+  |
+  | Tree: v
+  | I tried to show that
+  |   (v : String & Long)
+  | conforms to
+  |   String & Integer & List[String]
+  | but none of the attempts shown below succeeded:
+  |
+  |   ==> (v : String & Long)  <:  String & Integer & List[String]
+  |     ==> (v : String & Long)  <:  String & Integer
+  |       ==> (v : String & Long)  <:  Integer
+  |         ==> String & Long  <:  Integer
+  |           ==> String  <:  Integer  = false
+  |           ==> Long  <:  Integer  = false
+  |
+  | The tests were made under the empty constraint
+   ---------------------------------------------------------------------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg/i18737.scala:6:36 -------------------------------------------------------------
+6 |def test4(v: String | Long) = test3(v)  // error
+  |                                    ^
+  |                                    Found:    (v : String | Long)
+  |                                    Required: String | Integer | List[String]
+  |---------------------------------------------------------------------------------------------------------------------
+  | Explanation (enabled by `-explain`)
+  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+  |
+  | Tree: v
+  | I tried to show that
+  |   (v : String | Long)
+  | conforms to
+  |   String | Integer | List[String]
+  | but none of the attempts shown below succeeded:
+  |
+  |   ==> (v : String | Long)  <:  String | Integer | List[String]
+  |     ==> String | Long  <:  String | Integer | List[String]
+  |       ==> Long  <:  String | Integer | List[String]
+  |         ==> Long  <:  String | Integer
+  |           ==> Long  <:  String  = false
+  |           ==> Long  <:  Integer  = false
+  |         ==> Long  <:  List[String]  = false
+  |     ==> (v : String | Long)  <:  String | Integer
+  |       ==> String | Long  <:  String | Integer
+  |         ==> Long  <:  String | Integer
+  |           ==> Long  <:  String  = false
+  |           ==> Long  <:  Integer  = false
+  |       ==> (v : String | Long)  <:  String
+  |         ==> String | Long  <:  String
+  |           ==> Long  <:  String  = false
+  |       ==> (v : String | Long)  <:  Integer
+  |         ==> String | Long  <:  Integer
+  |           ==> String  <:  Integer  = false
+  |       ==> String | Long  <:  String | Integer
+  |         ==> Long  <:  String | Integer
+  |           ==> Long  <:  String  = false
+  |           ==> Long  <:  Integer  = false
+  |     ==> (v : String | Long)  <:  List[String]
+  |       ==> String | Long  <:  List[String]
+  |         ==> String  <:  List[String]  = false
+  |     ==> String | Long  <:  String | Integer | List[String]
+  |       ==> Long  <:  String | Integer | List[String]
+  |         ==> Long  <:  String | Integer
+  |           ==> Long  <:  String  = false
+  |           ==> Long  <:  Integer  = false
+  |         ==> Long  <:  List[String]  = false
+  |
+  | The tests were made under the empty constraint
+   ---------------------------------------------------------------------------------------------------------------------
diff --git a/tests/neg/i18737.scala b/tests/neg/i18737.scala
@@ -0,0 +1,6 @@
+//> using options -explain
+def test1(v: String & Integer & List[String]) = ()
+def test2(v: String & Long) = test1(v)  // error
+
+def test3(v: String | Integer | List[String]) = ()
+def test4(v: String | Long) = test3(v)  // error