From 5a7eab71ef65c77578fa7cd4df23142f00f1a1b7 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 12 Nov 2025 19:38:14 +0100 Subject: [PATCH 01/19] Implement sub-diagnostics --- .../tools/dotc/reporting/Diagnostic.scala | 20 +++++++- .../dotc/reporting/MessageRendering.scala | 50 +++++++++++++------ 2 files changed, 54 insertions(+), 16 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala index a4c30b4658e9..90b841a1adcb 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala @@ -11,6 +11,8 @@ import dotty.tools.dotc.util.chaining.* import java.util.{Collections, Optional, List => JList} import core.Decorators.toMessage +import collection.mutable.ArrayBuffer + object Diagnostic: def shouldExplain(dia: Diagnostic)(using Context): Boolean = @@ -117,6 +119,22 @@ class Diagnostic( msg.message.replaceAll("\u001B\\[[;\\d]*m", "") override def diagnosticRelatedInformation: JList[interfaces.DiagnosticRelatedInformation] = Collections.emptyList() - override def toString: String = s"$getClass at $pos L${pos.line+1}: $message" + + private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty + + def addSubdiag(diag: Subdiagnostic): Unit = + subdiags += diag + + def addSubdiag(msg: Message, pos: SourcePosition): Unit = + addSubdiag(Subdiagnostic(msg, pos)) + + def withSubdiags(diags: List[Subdiagnostic]): this.type = + diags.foreach(addSubdiag) + this + + def getSubdiags: List[Subdiagnostic] = subdiags.toList end Diagnostic + +class Subdiagnostic(val msg: Message, val pos: SourcePosition) + diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index 9366050a5a17..68b4b74089f2 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -77,10 +77,11 @@ trait MessageRendering { * -- Error: source.scala --------------------- * ``` */ - private def boxTitle(title: String)(using Context, Level, Offset): String = + private def boxTitle(title: String, isSubtitle: Boolean = false)(using Context, Level, Offset): String = val pageWidth = ctx.settings.pageWidth.value val line = "-" * (pageWidth - title.length - 4) - hl(s"-- $title $line") + val starter = if isSubtitle then ".." else "--" + hl(s"$starter $title $line") /** The position markers aligned under the error * @@ -169,7 +170,8 @@ trait MessageRendering { private def posStr( pos: SourcePosition, message: Message, - diagnosticString: String + diagnosticString: String, + isSubdiag: Boolean = false )(using Context, Level, Offset): String = assert( message.errorId.isActive, @@ -191,7 +193,7 @@ trait MessageRendering { val title = if fileAndPos.isEmpty then s"$errId$kind:" // this happens in dotty.tools.repl.ScriptedTests // TODO add name of source or remove `:` (and update test files) else s"$errId$kind: $fileAndPos" - boxTitle(title) + boxTitle(title, isSubtitle = isSubdiag) }) else "" end posStr @@ -232,6 +234,18 @@ trait MessageRendering { if origin.nonEmpty then addHelp("origin=")(origin) + // adjust a pos at EOF if preceded by newline + private def adjust(pos: SourcePosition): SourcePosition = + if pos.span.isSynthetic + && pos.span.isZeroExtent + && pos.span.exists + && pos.span.start == pos.source.length + && pos.source(pos.span.start - 1) == '\n' + then + pos.withSpan(pos.span.shift(-1)) + else + pos + /** The whole message rendered from `dia.msg`. * * For a position in an inline expansion, choose `pos1` @@ -252,17 +266,6 @@ trait MessageRendering { * */ def messageAndPos(dia: Diagnostic)(using Context): String = - // adjust a pos at EOF if preceded by newline - def adjust(pos: SourcePosition): SourcePosition = - if pos.span.isSynthetic - && pos.span.isZeroExtent - && pos.span.exists - && pos.span.start == pos.source.length - && pos.source(pos.span.start - 1) == '\n' - then - pos.withSpan(pos.span.shift(-1)) - else - pos val msg = dia.msg val pos = dia.pos val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos @@ -296,6 +299,9 @@ trait MessageRendering { sb.append(EOL).append(endBox) end if else sb.append(msg.message) + + dia.getSubdiags.foreach(addSubdiagnostic(sb, _)) + if dia.isVerbose then appendFilterHelp(dia, sb) @@ -313,6 +319,20 @@ trait MessageRendering { sb.toString end messageAndPos + private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit = + val pos1 = adjust(subdiag.pos) + val msg = subdiag.msg + assert(pos1.exists && pos1.source.file.exists) + + val posString = posStr(pos1, msg, "Note", isSubdiag = true) + val (srcBefore, srcAfter, offset) = sourceLines(pos1) + val marker = positionMarker(pos1) + val err = errorMsg(pos1, msg.message) + + val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL) + sb.append(EOL) + sb.append(diagText) + private def hl(str: String)(using Context, Level): String = summon[Level].value match case interfaces.Diagnostic.ERROR => Red(str).show From f3ec0a67b78ed0e1c1c17c52b9258e6c126b1826 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 12 Nov 2025 19:38:25 +0100 Subject: [PATCH 02/19] Use sub-diagnostics for consume error --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 6f1070c7ddea..ee773f48f4de 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -454,6 +454,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |No clashing definitions were found. This might point to an internal error.""", tree.srcPos) + class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error( + em"""Separation failure: Illegal access to $ref, which was consumed + |and therefore is no longer available.""", + useLoc.sourcePos + ): + addSubdiag(em"""$ref was passed to a consume parameter or + |was used as a prefix of a consume method here.""", consumedLoc.sourcePos) + /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed * @param loc the position where the capability was consumed @@ -465,6 +473,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed} |on line ${locPos.line + 1} and therefore is no longer available.""", pos) + // def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit = + // ctx.reporter.report(UseAfterConsume(ref, loc, pos)) /** Report a failure where a capability is consumed in a loop. * @param ref the capability From ed5c6674e4b6848c8bfba836bc132d00e7a4142e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 13 Nov 2025 13:57:08 +0100 Subject: [PATCH 03/19] Tweak the error message --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index ee773f48f4de..bde9ccdd33d3 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -455,12 +455,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: tree.srcPos) class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error( - em"""Separation failure: Illegal access to $ref, which was consumed + em"""Separation failure: Illegal access to $ref, which was passed to a + |consume parameter or was used as a prefix to a consume method |and therefore is no longer available.""", useLoc.sourcePos ): - addSubdiag(em"""$ref was passed to a consume parameter or - |was used as a prefix of a consume method here.""", consumedLoc.sourcePos) + addSubdiag(em"... $ref was consumed here.", consumedLoc.sourcePos) /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed From 4403ce067d7a827afdef655a3ab2150e0ac27298 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 20 Nov 2025 00:40:26 +0100 Subject: [PATCH 04/19] First prototype of all-in-one multi-span rendering --- .../dotc/reporting/MessageRendering.scala | 207 ++++++++++++++---- 1 file changed, 165 insertions(+), 42 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index 68b4b74089f2..af6b9e0e5718 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -246,65 +246,113 @@ trait MessageRendering { else pos - /** The whole message rendered from `dia.msg`. - * - * For a position in an inline expansion, choose `pos1` - * which is the most specific position in the call written - * by the user. For a diagnostic at EOF, where the last char - * of source text is a newline, adjust the position to render - * before the newline, at the end of the last line of text. - * - * The rendering begins with a label and position (`posString`). - * Then `sourceLines` with embedded caret `positionMarker` - * and rendered message. - * - * Then an `Inline stack trace` showing context for inlined code. - * Inlined positions are taken which don't contain `pos1`. - * (That should probably be positions not contained by outermost.) - * Note that position equality includes `outer` position; - * usually we intend to test `contains` or `coincidesWith`. - * - */ - def messageAndPos(dia: Diagnostic)(using Context): String = + /** Render diagnostics with positions in different files separately */ + private def renderSeparateSpans(dia: Diagnostic)(using Context): String = val msg = dia.msg val pos = dia.pos - val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos - val outermost = pos.outermost // call.pos - val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_)) + val pos1 = adjust(pos.nonInlined) given Level = Level(dia.level) given Offset = - val maxLineNumber = - if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1 - else 0 + val maxLineNumber = if pos.exists then pos1.endLine + 1 else 0 Offset(maxLineNumber.toString.length + 2) + val sb = StringBuilder() val posString = posStr(pos1, msg, diagnosticLevel(dia)) if posString.nonEmpty then sb.append(posString).append(EOL) + if pos.exists && pos1.exists && pos1.source.file.exists then val (srcBefore, srcAfter, offset) = sourceLines(pos1) val marker = positionMarker(pos1) val err = errorMsg(pos1, msg.message) sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL)) - - if inlineStack.nonEmpty then - sb.append(EOL).append(newBox()) - sb.append(EOL).append(offsetBox).append(i"Inline stack trace") - for inlinedPos <- inlineStack do - sb.append(EOL).append(newBox(soft = true)) - sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos") - if inlinedPos.source.file.exists then - val (srcBefore, srcAfter, _) = sourceLines(inlinedPos) - val marker = positionMarker(inlinedPos) - sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL)) - sb.append(EOL).append(endBox) - end if - else sb.append(msg.message) + else + sb.append(msg.message) dia.getSubdiags.foreach(addSubdiagnostic(sb, _)) + sb.toString + + def messageAndPosMultiSpan(dia: Diagnostic)(using Context): String = + val msg = dia.msg + val pos = dia.pos + val pos1 = adjust(pos.nonInlined) + val subdiags = dia.getSubdiags + + // Collect all positions with their associated messages + case class PosAndMsg(pos: SourcePosition, msg: Message, isPrimary: Boolean) + val allPosAndMsg = PosAndMsg(pos1, msg, true) :: subdiags.map(s => PosAndMsg(adjust(s.pos), s.msg, false)) + val validPosAndMsg = allPosAndMsg.filter(_.pos.exists) + + if validPosAndMsg.isEmpty then + return msg.message + + // Check all positions are in the same source file + val source = validPosAndMsg.head.pos.source + if !validPosAndMsg.forall(_.pos.source == source) || !source.file.exists then + // Cannot render multi-span if positions are in different files + // Fall back to showing them separately + return renderSeparateSpans(dia) + + // Find the line range covering all positions + val minLine = validPosAndMsg.map(_.pos.startLine).min + val maxLine = validPosAndMsg.map(_.pos.endLine).max + val maxLineNumber = maxLine + 1 + + given Level = Level(dia.level) + given Offset = Offset(maxLineNumber.toString.length + 2) + + val sb = StringBuilder() + + // Title using the primary position + val posString = posStr(pos1, msg, diagnosticLevel(dia)) + if posString.nonEmpty then sb.append(posString).append(EOL) + + // Render the unified code snippet + // Get syntax-highlighted content for the entire range + val startOffset = source.lineToOffset(minLine) + val endOffset = source.nextLine(source.lineToOffset(maxLine)) + val content = source.content.slice(startOffset, endOffset) + val syntax = + if (summon[Context].settings.color.value != "never" && !summon[Context].isJava) + SyntaxHighlighting.highlight(new String(content)).toCharArray + else content + + // Split syntax-highlighted content into lines + def linesFrom(arr: Array[Char]): List[String] = { + def pred(c: Char) = (c: @switch) match { + case LF | CR | FF | SU => true + case _ => false + } + val (line, rest0) = arr.span(!pred(_)) + val (_, rest) = rest0.span(pred) + new String(line) :: { if (rest.isEmpty) Nil else linesFrom(rest) } + } - if dia.isVerbose then - appendFilterHelp(dia, sb) + val lines = linesFrom(syntax) + val lineNumberWidth = maxLineNumber.toString.length + + // Render each line with its markers and messages + for (lineNum <- minLine to maxLine) { + val lineIdx = lineNum - minLine + if lineIdx < lines.length then + val lineContent = lines(lineIdx) + val lineNbr = (lineNum + 1).toString + val linePrefix = String.format(s"%${lineNumberWidth}s |", lineNbr) + val lnum = hl(" " * math.max(0, offset - linePrefix.length - 1) + linePrefix) + sb.append(lnum).append(lineContent.stripLineEnd).append(EOL) + + // Find all positions that should show markers after this line + // A position shows its marker after its start line + val positionsOnLine = validPosAndMsg.filter(_.pos.startLine == lineNum) + .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column + + for posAndMsg <- positionsOnLine do + val marker = positionMarker(posAndMsg.pos) + val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message) + sb.append(marker).append(EOL) + sb.append(err).append(EOL) + } + // Add explanation if needed if Diagnostic.shouldExplain(dia) then sb.append(EOL).append(newBox()) sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)") @@ -317,6 +365,81 @@ trait MessageRendering { sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`") sb.toString + end messageAndPosMultiSpan + + /** The whole message rendered from `dia.msg`. + * + * For a position in an inline expansion, choose `pos1` + * which is the most specific position in the call written + * by the user. For a diagnostic at EOF, where the last char + * of source text is a newline, adjust the position to render + * before the newline, at the end of the last line of text. + * + * The rendering begins with a label and position (`posString`). + * Then `sourceLines` with embedded caret `positionMarker` + * and rendered message. + * + * Then an `Inline stack trace` showing context for inlined code. + * Inlined positions are taken which don't contain `pos1`. + * (That should probably be positions not contained by outermost.) + * Note that position equality includes `outer` position; + * usually we intend to test `contains` or `coincidesWith`. + * + */ + def messageAndPos(dia: Diagnostic)(using Context): String = + if dia.getSubdiags.nonEmpty then messageAndPosMultiSpan(dia) + else + val msg = dia.msg + val pos = dia.pos + val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos + val outermost = pos.outermost // call.pos + val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_)) + given Level = Level(dia.level) + given Offset = + val maxLineNumber = + if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1 + else 0 + Offset(maxLineNumber.toString.length + 2) + val sb = StringBuilder() + val posString = posStr(pos1, msg, diagnosticLevel(dia)) + if posString.nonEmpty then sb.append(posString).append(EOL) + if pos.exists && pos1.exists && pos1.source.file.exists then + val (srcBefore, srcAfter, offset) = sourceLines(pos1) + val marker = positionMarker(pos1) + val err = errorMsg(pos1, msg.message) + sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL)) + + if inlineStack.nonEmpty then + sb.append(EOL).append(newBox()) + sb.append(EOL).append(offsetBox).append(i"Inline stack trace") + for inlinedPos <- inlineStack do + sb.append(EOL).append(newBox(soft = true)) + sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos") + if inlinedPos.source.file.exists then + val (srcBefore, srcAfter, _) = sourceLines(inlinedPos) + val marker = positionMarker(inlinedPos) + sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL)) + sb.append(EOL).append(endBox) + end if + else sb.append(msg.message) + + dia.getSubdiags.foreach(addSubdiagnostic(sb, _)) + + if dia.isVerbose then + appendFilterHelp(dia, sb) + + if Diagnostic.shouldExplain(dia) then + sb.append(EOL).append(newBox()) + sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)") + sb.append(EOL).append(newBox(soft = true)) + dia.msg.explanation.split(raw"\R").foreach: line => + sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line) + sb.append(EOL).append(endBox) + else if dia.msg.canExplain then + sb.append(EOL).append(offsetBox) + sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`") + + sb.toString end messageAndPos private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit = From 0c91750ed2de7d21311fe94d1b46fe55e118d880 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 20 Nov 2025 00:43:55 +0100 Subject: [PATCH 05/19] Use `---` for secondary messages --- .../dotc/reporting/MessageRendering.scala | 23 +++++++++++++------ 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index af6b9e0e5718..4a78f6b41403 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -88,14 +88,21 @@ trait MessageRendering { * ``` * | ^^^^^ * ``` + * or for sub-diagnostics: + * ``` + * | ----- + * ``` + * + * @param pos the source position to mark + * @param markerChar the character to use for marking ('^' for primary errors, '-' for notes) */ - private def positionMarker(pos: SourcePosition)(using Context, Level, Offset): String = { + private def positionMarker(pos: SourcePosition, markerChar: Char = '^')(using Context, Level, Offset): String = { val padding = pos.startColumnPadding - val carets = + val markers = if (pos.startLine == pos.endLine) - "^" * math.max(1, pos.endColumn - pos.startColumn) - else "^" - hl(s"$offsetBox$padding$carets") + markerChar.toString * math.max(1, pos.endColumn - pos.startColumn) + else markerChar.toString + hl(s"$offsetBox$padding$markers") } /** The horizontal line with the given offset @@ -346,7 +353,9 @@ trait MessageRendering { .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column for posAndMsg <- positionsOnLine do - val marker = positionMarker(posAndMsg.pos) + // Use '^' for primary error, '-' for sub-diagnostics + val markerChar = if posAndMsg.isPrimary then '^' else '-' + val marker = positionMarker(posAndMsg.pos, markerChar) val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message) sb.append(marker).append(EOL) sb.append(err).append(EOL) @@ -449,7 +458,7 @@ trait MessageRendering { val posString = posStr(pos1, msg, "Note", isSubdiag = true) val (srcBefore, srcAfter, offset) = sourceLines(pos1) - val marker = positionMarker(pos1) + val marker = positionMarker(pos1, '-') // Use '-' for sub-diagnostics val err = errorMsg(pos1, msg.message) val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL) From 5ad8825fa542b04f00a0952420a021171bfd0cfe Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 20 Nov 2025 00:52:11 +0100 Subject: [PATCH 06/19] Display primary error message before multi-span error --- .../src/dotty/tools/dotc/reporting/MessageRendering.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index 4a78f6b41403..b907cbf24ac1 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -313,6 +313,10 @@ trait MessageRendering { val posString = posStr(pos1, msg, diagnosticLevel(dia)) if posString.nonEmpty then sb.append(posString).append(EOL) + // Display primary error message before code snippet + sb.append(msg.message) + if !msg.message.endsWith(EOL) then sb.append(EOL) + // Render the unified code snippet // Get syntax-highlighted content for the entire range val startOffset = source.lineToOffset(minLine) From eb5aa1b016c35d5be479de622cccdf5da3b4f3cc Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 20 Nov 2025 01:05:37 +0100 Subject: [PATCH 07/19] Multi-span error reporting for consume errors --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 3 ++- .../src/dotty/tools/dotc/reporting/Diagnostic.scala | 9 +++++++++ .../dotty/tools/dotc/reporting/MessageRendering.scala | 11 +++++++---- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index bde9ccdd33d3..34fd5729a34b 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -460,7 +460,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |and therefore is no longer available.""", useLoc.sourcePos ): - addSubdiag(em"... $ref was consumed here.", consumedLoc.sourcePos) + addSubdiag(em"$ref was consumed here.", consumedLoc.sourcePos) + addPrimaryNote(em"... and it was used here") /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala index 90b841a1adcb..dc635c01015a 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala @@ -123,9 +123,18 @@ class Diagnostic( private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty + private var primaryNote: Message | Null = null + def addSubdiag(diag: Subdiagnostic): Unit = subdiags += diag + def addPrimaryNote(msg: Message): Unit = + assert(primaryNote eq null) + primaryNote = msg + + def getPrimaryNote: Option[Message] = + if primaryNote eq null then None else Some(primaryNote.nn) + def addSubdiag(msg: Message, pos: SourcePosition): Unit = addSubdiag(Subdiagnostic(msg, pos)) diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index b907cbf24ac1..838ad358f4ca 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -313,7 +313,7 @@ trait MessageRendering { val posString = posStr(pos1, msg, diagnosticLevel(dia)) if posString.nonEmpty then sb.append(posString).append(EOL) - // Display primary error message before code snippet + // Always display primary error message before code snippet sb.append(msg.message) if !msg.message.endsWith(EOL) then sb.append(EOL) @@ -342,7 +342,7 @@ trait MessageRendering { val lineNumberWidth = maxLineNumber.toString.length // Render each line with its markers and messages - for (lineNum <- minLine to maxLine) { + for (lineNum <- minLine to maxLine) do val lineIdx = lineNum - minLine if lineIdx < lines.length then val lineContent = lines(lineIdx) @@ -360,10 +360,13 @@ trait MessageRendering { // Use '^' for primary error, '-' for sub-diagnostics val markerChar = if posAndMsg.isPrimary then '^' else '-' val marker = positionMarker(posAndMsg.pos, markerChar) - val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message) + // For primary position: use PrimaryNote if available, otherwise use primary message + val messageToShow = + if posAndMsg.isPrimary then dia.getPrimaryNote.map(_.message).getOrElse(posAndMsg.msg.message) + else posAndMsg.msg.message + val err = errorMsg(posAndMsg.pos, messageToShow) sb.append(marker).append(EOL) sb.append(err).append(EOL) - } // Add explanation if needed if Diagnostic.shouldExplain(dia) then From a27db397123204e15ac33f0bcf7633cbed7d0392 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 20 Nov 2025 01:07:30 +0100 Subject: [PATCH 08/19] Tweak the error message --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 34fd5729a34b..0ab3df95b4b7 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -460,8 +460,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |and therefore is no longer available.""", useLoc.sourcePos ): - addSubdiag(em"$ref was consumed here.", consumedLoc.sourcePos) - addPrimaryNote(em"... and it was used here") + addSubdiag(em"The capability was consumed here.", consumedLoc.sourcePos) + addPrimaryNote(em"Then, it was used here") /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed From e412f1190b2b30132a936f3719a33b025813bf6e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 21 Nov 2025 17:25:03 +0100 Subject: [PATCH 09/19] Refactor: move multi-span handling logic to Message --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 35 ++++-- .../tools/dotc/reporting/Diagnostic.scala | 27 ----- .../dotty/tools/dotc/reporting/Message.scala | 18 +++ .../dotc/reporting/MessageRendering.scala | 107 ++++++------------ 4 files changed, 75 insertions(+), 112 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 0ab3df95b4b7..5ab75eb8b6bf 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -454,14 +454,31 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |No clashing definitions were found. This might point to an internal error.""", tree.srcPos) - class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error( - em"""Separation failure: Illegal access to $ref, which was passed to a - |consume parameter or was used as a prefix to a consume method - |and therefore is no longer available.""", - useLoc.sourcePos - ): - addSubdiag(em"The capability was consumed here.", consumedLoc.sourcePos) - addPrimaryNote(em"Then, it was used here") + class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Message(reporting.ErrorMessageID.NoExplanationID): + def kind = reporting.MessageKind.NoKind + + protected def msg(using Context): String = "" + + protected def explain(using Context): String = "" + + override def leading(using Context): Option[String] = Some( + em"""Separation failure: Illegal access to $ref, which was passed to a + |consume parameter or was used as a prefix to a consume method + |and therefore is no longer available.""".message + ) + + override def parts(using Context): List[reporting.Message.MessagePart] = List( + reporting.Message.MessagePart( + "The capability was consumed here.", + consumedLoc.sourcePos, + isPrimary = false + ), + reporting.Message.MessagePart( + "Then, it was used here", + useLoc.sourcePos, + isPrimary = true + ) + ) /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed @@ -474,8 +491,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed} |on line ${locPos.line + 1} and therefore is no longer available.""", pos) - // def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit = - // ctx.reporter.report(UseAfterConsume(ref, loc, pos)) /** Report a failure where a capability is consumed in a loop. * @param ref the capability diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala index dc635c01015a..807185106d01 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala @@ -11,8 +11,6 @@ import dotty.tools.dotc.util.chaining.* import java.util.{Collections, Optional, List => JList} import core.Decorators.toMessage -import collection.mutable.ArrayBuffer - object Diagnostic: def shouldExplain(dia: Diagnostic)(using Context): Boolean = @@ -120,30 +118,5 @@ class Diagnostic( override def diagnosticRelatedInformation: JList[interfaces.DiagnosticRelatedInformation] = Collections.emptyList() override def toString: String = s"$getClass at $pos L${pos.line+1}: $message" - - private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty - - private var primaryNote: Message | Null = null - - def addSubdiag(diag: Subdiagnostic): Unit = - subdiags += diag - - def addPrimaryNote(msg: Message): Unit = - assert(primaryNote eq null) - primaryNote = msg - - def getPrimaryNote: Option[Message] = - if primaryNote eq null then None else Some(primaryNote.nn) - - def addSubdiag(msg: Message, pos: SourcePosition): Unit = - addSubdiag(Subdiagnostic(msg, pos)) - - def withSubdiags(diags: List[Subdiagnostic]): this.type = - diags.foreach(addSubdiag) - this - - def getSubdiags: List[Subdiagnostic] = subdiags.toList end Diagnostic -class Subdiagnostic(val msg: Message, val pos: SourcePosition) - diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala index 1c71b7468c0b..1a542ca0dbdd 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Message.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala @@ -300,6 +300,13 @@ object Message: super.toText(sym) end Printer + /** A part of a multi-span message, associating text with a source position. + * @param text the message text for this part + * @param srcPos the source position where this part applies + * @param isPrimary whether this is the primary message (true) or a secondary note (false) + */ + case class MessagePart(text: String, srcPos: util.SourcePosition, isPrimary: Boolean) + end Message /** A `Message` contains all semantic information necessary to easily @@ -370,6 +377,17 @@ abstract class Message(val errorId: ErrorMessageID)(using Context) { self => */ protected def explain(using Context): String + /** Optional leading text to be displayed before the source snippet. + * If present along with parts, triggers multi-span rendering. + */ + def leading(using Context): Option[String] = None + + /** Optional list of message parts for multi-span error messages. + * Each part associates text with a source position and indicates + * whether it's a primary message or a secondary note. + */ + def parts(using Context): List[MessagePart] = Nil + /** What gets printed after the message proper */ protected def msgPostscript(using Context): String = if ctx eq NoContext then "" diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index 838ad358f4ca..4b94a605f49b 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -253,55 +253,31 @@ trait MessageRendering { else pos - /** Render diagnostics with positions in different files separately */ - private def renderSeparateSpans(dia: Diagnostic)(using Context): String = + /** Render a message using multi-span information from Message.parts. */ + def messageAndPosFromParts(dia: Diagnostic)(using Context): String = val msg = dia.msg val pos = dia.pos val pos1 = adjust(pos.nonInlined) - given Level = Level(dia.level) - given Offset = - val maxLineNumber = if pos.exists then pos1.endLine + 1 else 0 - Offset(maxLineNumber.toString.length + 2) - - val sb = StringBuilder() - val posString = posStr(pos1, msg, diagnosticLevel(dia)) - if posString.nonEmpty then sb.append(posString).append(EOL) + val msgParts = msg.parts - if pos.exists && pos1.exists && pos1.source.file.exists then - val (srcBefore, srcAfter, offset) = sourceLines(pos1) - val marker = positionMarker(pos1) - val err = errorMsg(pos1, msg.message) - sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL)) - else - sb.append(msg.message) + if msgParts.isEmpty then + return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message - dia.getSubdiags.foreach(addSubdiagnostic(sb, _)) - sb.toString + // Collect all positions from message parts + val validParts = msgParts.filter(_.srcPos.exists) - def messageAndPosMultiSpan(dia: Diagnostic)(using Context): String = - val msg = dia.msg - val pos = dia.pos - val pos1 = adjust(pos.nonInlined) - val subdiags = dia.getSubdiags - - // Collect all positions with their associated messages - case class PosAndMsg(pos: SourcePosition, msg: Message, isPrimary: Boolean) - val allPosAndMsg = PosAndMsg(pos1, msg, true) :: subdiags.map(s => PosAndMsg(adjust(s.pos), s.msg, false)) - val validPosAndMsg = allPosAndMsg.filter(_.pos.exists) - - if validPosAndMsg.isEmpty then - return msg.message + if validParts.isEmpty then + return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message // Check all positions are in the same source file - val source = validPosAndMsg.head.pos.source - if !validPosAndMsg.forall(_.pos.source == source) || !source.file.exists then - // Cannot render multi-span if positions are in different files - // Fall back to showing them separately - return renderSeparateSpans(dia) + val source = validParts.head.srcPos.source + if !validParts.forall(_.srcPos.source == source) || !source.file.exists then + // TODO: support rendering source positions across multiple files + return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message // Find the line range covering all positions - val minLine = validPosAndMsg.map(_.pos.startLine).min - val maxLine = validPosAndMsg.map(_.pos.endLine).max + val minLine = validParts.map(_.srcPos.startLine).min + val maxLine = validParts.map(_.srcPos.endLine).max val maxLineNumber = maxLine + 1 given Level = Level(dia.level) @@ -313,12 +289,13 @@ trait MessageRendering { val posString = posStr(pos1, msg, diagnosticLevel(dia)) if posString.nonEmpty then sb.append(posString).append(EOL) - // Always display primary error message before code snippet - sb.append(msg.message) - if !msg.message.endsWith(EOL) then sb.append(EOL) + // Display leading text if present + msg.leading.foreach { leadingText => + sb.append(leadingText) + if !leadingText.endsWith(EOL) then sb.append(EOL) + } // Render the unified code snippet - // Get syntax-highlighted content for the entire range val startOffset = source.lineToOffset(minLine) val endOffset = source.nextLine(source.lineToOffset(maxLine)) val content = source.content.slice(startOffset, endOffset) @@ -352,19 +329,13 @@ trait MessageRendering { sb.append(lnum).append(lineContent.stripLineEnd).append(EOL) // Find all positions that should show markers after this line - // A position shows its marker after its start line - val positionsOnLine = validPosAndMsg.filter(_.pos.startLine == lineNum) - .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column - - for posAndMsg <- positionsOnLine do - // Use '^' for primary error, '-' for sub-diagnostics - val markerChar = if posAndMsg.isPrimary then '^' else '-' - val marker = positionMarker(posAndMsg.pos, markerChar) - // For primary position: use PrimaryNote if available, otherwise use primary message - val messageToShow = - if posAndMsg.isPrimary then dia.getPrimaryNote.map(_.message).getOrElse(posAndMsg.msg.message) - else posAndMsg.msg.message - val err = errorMsg(posAndMsg.pos, messageToShow) + val partsOnLine = validParts.filter(_.srcPos.startLine == lineNum) + .sortBy(p => (p.srcPos.startColumn, !p.isPrimary)) + + for part <- partsOnLine do + val markerChar = if part.isPrimary then '^' else '-' + val marker = positionMarker(part.srcPos, markerChar) + val err = errorMsg(part.srcPos, part.text) sb.append(marker).append(EOL) sb.append(err).append(EOL) @@ -381,7 +352,7 @@ trait MessageRendering { sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`") sb.toString - end messageAndPosMultiSpan + end messageAndPosFromParts /** The whole message rendered from `dia.msg`. * @@ -403,9 +374,11 @@ trait MessageRendering { * */ def messageAndPos(dia: Diagnostic)(using Context): String = - if dia.getSubdiags.nonEmpty then messageAndPosMultiSpan(dia) + val msg = dia.msg + // Check if message provides its own multi-span structure + if msg.leading.isDefined || msg.parts.nonEmpty then + messageAndPosFromParts(dia) else - val msg = dia.msg val pos = dia.pos val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos val outermost = pos.outermost // call.pos @@ -439,8 +412,6 @@ trait MessageRendering { end if else sb.append(msg.message) - dia.getSubdiags.foreach(addSubdiagnostic(sb, _)) - if dia.isVerbose then appendFilterHelp(dia, sb) @@ -458,20 +429,6 @@ trait MessageRendering { sb.toString end messageAndPos - private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit = - val pos1 = adjust(subdiag.pos) - val msg = subdiag.msg - assert(pos1.exists && pos1.source.file.exists) - - val posString = posStr(pos1, msg, "Note", isSubdiag = true) - val (srcBefore, srcAfter, offset) = sourceLines(pos1) - val marker = positionMarker(pos1, '-') // Use '-' for sub-diagnostics - val err = errorMsg(pos1, msg.message) - - val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL) - sb.append(EOL) - sb.append(diagText) - private def hl(str: String)(using Context, Level): String = summon[Level].value match case interfaces.Diagnostic.ERROR => Red(str).show From b3fcdba9db0ff0ea188866759d20dc14bec6877c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 21 Nov 2025 17:39:43 +0100 Subject: [PATCH 10/19] Move UseAfterConsume to messages.scala --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 26 ------------------- .../dotty/tools/dotc/reporting/messages.scala | 24 +++++++++++++++++ 2 files changed, 24 insertions(+), 26 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 5ab75eb8b6bf..6f1070c7ddea 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -454,32 +454,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |No clashing definitions were found. This might point to an internal error.""", tree.srcPos) - class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Message(reporting.ErrorMessageID.NoExplanationID): - def kind = reporting.MessageKind.NoKind - - protected def msg(using Context): String = "" - - protected def explain(using Context): String = "" - - override def leading(using Context): Option[String] = Some( - em"""Separation failure: Illegal access to $ref, which was passed to a - |consume parameter or was used as a prefix to a consume method - |and therefore is no longer available.""".message - ) - - override def parts(using Context): List[reporting.Message.MessagePart] = List( - reporting.Message.MessagePart( - "The capability was consumed here.", - consumedLoc.sourcePos, - isPrimary = false - ), - reporting.Message.MessagePart( - "Then, it was used here", - useLoc.sourcePos, - isPrimary = true - ) - ) - /** Report a failure where a previously consumed capability is used again, * @param ref the capability that is used after being consumed * @param loc the position where the capability was consumed diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala index 159b3c9a905e..73d13acb12b8 100644 --- a/compiler/src/dotty/tools/dotc/reporting/messages.scala +++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala @@ -3749,3 +3749,27 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco |or `myfile-test.scala` can produce encoded names for the generated package objects. | |In this case, the name `$name` is encoded as `${name.encode}`.""" + +class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition)(using Context) +extends TypeMsg(NoExplanationID): + protected def msg(using Context): String = + i"""Separation failure: Illegal access to $ref, which was passed to a + |consume parameter or was used as a prefix to a consume method + |and therefore is no longer available.""" + + protected def explain(using Context): String = "" + + override def leading(using Context): Option[String] = Some(message) + + override def parts(using Context): List[Message.MessagePart] = List( + Message.MessagePart( + "The capability was consumed here.", + consumedLoc, + isPrimary = false + ), + Message.MessagePart( + "Then, it was used here", + useLoc, + isPrimary = true + ) + ) From 539c3bdd1b7ddb5cde0c1b16d0f06bb45f1b6b0c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 22 Nov 2025 00:08:47 +0100 Subject: [PATCH 11/19] Add test for consume error --- tests/neg-custom-args/captures/consume-twice.check | 13 +++++++++++++ tests/neg-custom-args/captures/consume-twice.scala | 6 ++++++ 2 files changed, 19 insertions(+) create mode 100644 tests/neg-custom-args/captures/consume-twice.check create mode 100644 tests/neg-custom-args/captures/consume-twice.scala diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check new file mode 100644 index 000000000000..073a1459c9a4 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-twice.check @@ -0,0 +1,13 @@ +-- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 -------------------------------------------------- +Separation failure: Illegal access to (x : Object^), which was passed to a +consume parameter or was used as a prefix to a consume method +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +5 | send(x) + | - + | The capability was consumed here. +6 | send(x) // error + | ^ + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/consume-twice.scala b/tests/neg-custom-args/captures/consume-twice.scala new file mode 100644 index 000000000000..b0f955e9dbf7 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-twice.scala @@ -0,0 +1,6 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +def send(consume x: Object^): Unit = () +def consumeTwice(consume x: Object^): Unit = + send(x) + send(x) // error From 12694339e2c6bb6d217da0396928aa109d6679b3 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 22 Nov 2025 00:22:18 +0100 Subject: [PATCH 12/19] Support multi-parts on the same line --- .../dotc/reporting/MessageRendering.scala | 46 ++++++++++++++++++- .../captures/consume-twice-same-line.check | 33 +++++++++++++ .../captures/consume-twice-same-line.scala | 8 ++++ 3 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 tests/neg-custom-args/captures/consume-twice-same-line.check create mode 100644 tests/neg-custom-args/captures/consume-twice-same-line.scala diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index 4b94a605f49b..d59af43691fa 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -332,12 +332,56 @@ trait MessageRendering { val partsOnLine = validParts.filter(_.srcPos.startLine == lineNum) .sortBy(p => (p.srcPos.startColumn, !p.isPrimary)) - for part <- partsOnLine do + if partsOnLine.size == 1 then + // Single marker on this line + val part = partsOnLine.head val markerChar = if part.isPrimary then '^' else '-' val marker = positionMarker(part.srcPos, markerChar) val err = errorMsg(part.srcPos, part.text) sb.append(marker).append(EOL) sb.append(err).append(EOL) + else if partsOnLine.size > 1 then + // Multiple markers on same line + val markerLine = StringBuilder() + markerLine.append(offsetBox) + + var currentCol = 0 + for part <- partsOnLine do + val markerChar = if part.isPrimary then '^' else '-' + val targetCol = part.srcPos.startColumn + val padding = " " * (targetCol - currentCol) + markerLine.append(padding).append(markerChar) + currentCol = targetCol + 1 + + sb.append(markerLine).append(EOL) + + // Render messages from right to left with connector bars + val sortedByColumn = partsOnLine.reverse // rightmost first + for (part, idx) <- sortedByColumn.zipWithIndex do + val remainingParts = sortedByColumn.drop(idx + 1) // parts still waiting for messages + + // Build connector line with vertical bars for remaining parts + val connectorLine = StringBuilder() + connectorLine.append(offsetBox) + + var col = 0 + // First, add vertical bars for all remaining (not-yet-shown) parts + for p <- partsOnLine do + if remainingParts.contains(p) then + val targetCol = p.srcPos.startColumn + val padding = " " * (targetCol - col) + connectorLine.append(padding).append("|") + col = targetCol + 1 + + // Then add the message for the current part, aligned to its column + val msgText = part.text + val msgCol = part.srcPos.startColumn + // If we've added bars, col is position after last bar; if not, col is 0 + // We want the message to start at msgCol, with at least one space separation + val msgPadding = if col == 0 then " " * msgCol else " " * Math.max(1, msgCol - col) + connectorLine.append(msgPadding).append(msgText) + + sb.append(connectorLine).append(EOL) // Add explanation if needed if Diagnostic.shouldExplain(dia) then diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check new file mode 100644 index 000000000000..24a8a4734042 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-twice-same-line.check @@ -0,0 +1,33 @@ +-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 --------------------------------------- +Separation failure: Illegal access to (x : Object^), which was passed to a +consume parameter or was used as a prefix to a consume method +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +5 | send(x); send(x) // error + | - ^ + | | Then, it was used here + | The capability was consumed here. + +-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 --------------------------------------- +Separation failure: Illegal access to (x : Object^), which was passed to a +consume parameter or was used as a prefix to a consume method +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +8 | send(x); send(x); send(x) // error // error + | - ^ + | | Then, it was used here + | The capability was consumed here. + +-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 --------------------------------------- +Separation failure: Illegal access to (x : Object^), which was passed to a +consume parameter or was used as a prefix to a consume method +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +8 | send(x); send(x); send(x) // error // error + | - ^ + | | Then, it was used here + | The capability was consumed here. + diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.scala b/tests/neg-custom-args/captures/consume-twice-same-line.scala new file mode 100644 index 000000000000..858786419e16 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-twice-same-line.scala @@ -0,0 +1,8 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +def send(consume x: Object^): Unit = () +def consumeTwice(consume x: Object^): Unit = + send(x); send(x) // error + +def consumeThrice(consume x: Object^): Unit = + send(x); send(x); send(x) // error // error From 4ec34135a998bc2ef6021a634670c0fa05756a65 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 22 Nov 2025 00:32:47 +0100 Subject: [PATCH 13/19] Use precise consume reason --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 5 +---- compiler/src/dotty/tools/dotc/reporting/messages.scala | 5 ++--- .../captures/consume-twice-same-line.check | 9 +++------ tests/neg-custom-args/captures/consume-twice.check | 3 +-- 4 files changed, 7 insertions(+), 15 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 6f1070c7ddea..aea10c4911f8 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -461,10 +461,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: */ def consumeError(ref: Capability, loc: (SrcPos, TypeRole), pos: SrcPos)(using Context): Unit = val (locPos, role) = loc - report.error( - em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed} - |on line ${locPos.line + 1} and therefore is no longer available.""", - pos) + report.error(reporting.UseAfterConsume(ref, locPos.sourcePos, pos.sourcePos, role.howConsumed), pos) /** Report a failure where a capability is consumed in a loop. * @param ref the capability diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala index 73d13acb12b8..d76239f575d5 100644 --- a/compiler/src/dotty/tools/dotc/reporting/messages.scala +++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala @@ -3750,11 +3750,10 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco | |In this case, the name `$name` is encoded as `${name.encode}`.""" -class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition)(using Context) +class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) extends TypeMsg(NoExplanationID): protected def msg(using Context): String = - i"""Separation failure: Illegal access to $ref, which was passed to a - |consume parameter or was used as a prefix to a consume method + i"""Separation failure: Illegal access to $ref, which was $howConsumed |and therefore is no longer available.""" protected def explain(using Context): String = "" diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check index 24a8a4734042..d549f450be1d 100644 --- a/tests/neg-custom-args/captures/consume-twice-same-line.check +++ b/tests/neg-custom-args/captures/consume-twice-same-line.check @@ -1,6 +1,5 @@ -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 --------------------------------------- -Separation failure: Illegal access to (x : Object^), which was passed to a -consume parameter or was used as a prefix to a consume method +Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. where: ^ refers to a fresh root capability in the type of parameter x @@ -10,8 +9,7 @@ where: ^ refers to a fresh root capability in the type of parameter x | The capability was consumed here. -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 --------------------------------------- -Separation failure: Illegal access to (x : Object^), which was passed to a -consume parameter or was used as a prefix to a consume method +Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. where: ^ refers to a fresh root capability in the type of parameter x @@ -21,8 +19,7 @@ where: ^ refers to a fresh root capability in the type of parameter x | The capability was consumed here. -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 --------------------------------------- -Separation failure: Illegal access to (x : Object^), which was passed to a -consume parameter or was used as a prefix to a consume method +Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. where: ^ refers to a fresh root capability in the type of parameter x diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check index 073a1459c9a4..6f88f54a1d4d 100644 --- a/tests/neg-custom-args/captures/consume-twice.check +++ b/tests/neg-custom-args/captures/consume-twice.check @@ -1,6 +1,5 @@ -- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 -------------------------------------------------- -Separation failure: Illegal access to (x : Object^), which was passed to a -consume parameter or was used as a prefix to a consume method +Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. where: ^ refers to a fresh root capability in the type of parameter x From 1fe413d4f15c9bb51a4feff226e005f3116aea92 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 22 Nov 2025 14:32:52 +0100 Subject: [PATCH 14/19] Update checkfiles --- .../dotty/tools/dotc/reporting/messages.scala | 5 +- .../captures/linear-buffer-2.check | 56 ++++++++++++++++ .../captures/linear-buffer.check | 67 ++++++++++++++++++- .../captures/sep-consume.check | 26 +++++++ 4 files changed, 150 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala index d76239f575d5..e337c10b595c 100644 --- a/compiler/src/dotty/tools/dotc/reporting/messages.scala +++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala @@ -3750,8 +3750,9 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco | |In this case, the name `$name` is encoded as `${name.encode}`.""" -class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) -extends TypeMsg(NoExplanationID): +class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) extends Message(NoExplanationID): + def kind = MessageKind.NoKind + protected def msg(using Context): String = i"""Separation failure: Illegal access to $ref, which was $howConsumed |and therefore is no longer available.""" diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 6a3853770f4e..67dbff6bd419 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -1,31 +1,87 @@ -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 --------------------------------------------------- +Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter buf +11 | val buf1: Buffer[Int]^ = buf.append(1) + | --- + | The capability was consumed here. +12 | val buf2 = buf1.append(2) // OK 13 | val buf3 = buf.append(3) // error | ^^^ +<<<<<<< HEAD | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append | on line 11 and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +18 | if ??? then buf1.append(2) // OK + | ---- + | The capability was consumed here. +19 | else buf1.append(3) // OK 20 | val buf3 = buf1.append(4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 18 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +25 | case 1 => buf1.append(2) // OK + | ---- + | The capability was consumed here. +26 | case 2 => buf1.append(2) +27 | case _ => buf1.append(3) 28 | val buf3 = buf1.append(4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 25 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +33 | case 1 => buf1.append(2) // OK + | ---- + | The capability was consumed here. +34 | case 2 => buf1.append(2) +35 | case 3 => buf1.append(3) +36 | case 4 => buf1.append(4) +37 | case 5 => buf1.append(5) 38 | val buf3 = buf1.append(4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 33 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(1) // error | ^^^ diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 225792af4189..b0c90a038e15 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -34,33 +34,89 @@ | Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. | The access must be in a consume method to allow this. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 ----------------------------------------------------- +Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter buf +21 | val buf1: Buffer[Int]^ = app(buf, 1) + | --- + | The capability was consumed here. +22 | val buf2 = app(buf1, 2) // OK 23 | val buf3 = app(buf, 3) // error | ^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app |on line 21 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 ----------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +28 | if ??? then app(buf1, 2) // OK + | ---- + | The capability was consumed here. +29 | else app(buf1, 3) // OK 30 | val buf3 = app(buf1, 4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 28 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 ----------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +35 | case 1 => app(buf1, 2) // OK + | ---- + | The capability was consumed here. +36 | case 2 => app(buf1, 2) +37 | case _ => app(buf1, 3) 38 | val buf3 = app(buf1, 4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 35 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 ----------------------------------------------------- +Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value buf1 +43 | case 1 => app(buf1, 2) // OK + | ---- + | The capability was consumed here. +44 | case 2 => app(buf1, 2) +45 | case 3 => app(buf1, 3) +46 | case 4 => app(buf1, 4) +47 | case 5 => app(buf1, 5) 48 | val buf3 = app(buf1, 4) // error | ^^^^ +<<<<<<< HEAD |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 43 and therefore is no longer available. | |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------ 52 | app(buf, 1) // error | ^^^ @@ -69,7 +125,14 @@ | | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 ----------------------------------------------------- +Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app +and therefore is no longer available. +59 | val buf1 = app(buf, "hi") // buf unavailable from here + | --- + | The capability was consumed here. +60 | val c1 = contents(buf1) // only buf.rd is consumed +61 | val c2 = contents(buf1) // buf.rd can be consumed repeatedly 62 | val c3 = contents(buf) // error | ^^^ - | Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app - | on line 59 and therefore is no longer available. + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 40521e319b61..40e1643c8455 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -4,19 +4,45 @@ | Local reach capability p.fst* leaks into capture scope of method test4. | You could try to abstract the capabilities referred to by p.fst* in a capset variable. -- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 -------------------------------------------------------- +Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap` + | - + | The capability was consumed here. 19 | x.put(42) // error | ^ +<<<<<<< HEAD | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad | on line 18 and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- +Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter x +18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap` + | - + | The capability was consumed here. +19 | x.put(42) // error +20 | x.get // ok rd/rd 21 | par(rx, () => x.put(42)) // error | ^ +<<<<<<< HEAD | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad | on line 18 and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x +======= + | Then, it was used here + +>>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ From fa179d0927f30ae0af23d869b5b9c8226fb2517f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 9 Dec 2025 18:29:53 +0100 Subject: [PATCH 15/19] Multi-span error reporting for overriding --- .../dotc/reporting/MessageRendering.scala | 118 +++++++++++------- .../dotty/tools/dotc/reporting/messages.scala | 24 ++++ tests/neg/override-multi-file-error.check | 13 ++ tests/neg/override-multi-file-error/A.scala | 3 + tests/neg/override-multi-file-error/B.scala | 3 + tests/neg/override-multi-span.check | 14 +++ tests/neg/override-multi-span.scala | 6 + 7 files changed, 139 insertions(+), 42 deletions(-) create mode 100644 tests/neg/override-multi-file-error.check create mode 100644 tests/neg/override-multi-file-error/A.scala create mode 100644 tests/neg/override-multi-file-error/B.scala create mode 100644 tests/neg/override-multi-span.check create mode 100644 tests/neg/override-multi-span.scala diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index d59af43691fa..b2ddaccbfa95 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -12,7 +12,7 @@ import io.AbstractFile import printing.Highlighting.{Blue, Red, Yellow} import printing.SyntaxHighlighting import Diagnostic.* -import util.{SourcePosition, NoSourcePosition} +import util.{SourceFile, SourcePosition, NoSourcePosition} import util.Chars.{ LF, CR, FF, SU } import scala.annotation.switch @@ -253,47 +253,21 @@ trait MessageRendering { else pos - /** Render a message using multi-span information from Message.parts. */ - def messageAndPosFromParts(dia: Diagnostic)(using Context): String = - val msg = dia.msg - val pos = dia.pos - val pos1 = adjust(pos.nonInlined) - val msgParts = msg.parts - - if msgParts.isEmpty then - return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message - - // Collect all positions from message parts - val validParts = msgParts.filter(_.srcPos.exists) - - if validParts.isEmpty then - return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message + /** Render parts for a single source file. + * @param parts the message parts to render (all must be from the same source) + * @param sb the StringBuilder to append to + */ + private def renderPartsForFile( + parts: List[Message.MessagePart], + sb: StringBuilder + )(using Context, Level, Offset): Unit = + if parts.isEmpty then return - // Check all positions are in the same source file - val source = validParts.head.srcPos.source - if !validParts.forall(_.srcPos.source == source) || !source.file.exists then - // TODO: support rendering source positions across multiple files - return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message + val source = parts.head.srcPos.source // Find the line range covering all positions - val minLine = validParts.map(_.srcPos.startLine).min - val maxLine = validParts.map(_.srcPos.endLine).max - val maxLineNumber = maxLine + 1 - - given Level = Level(dia.level) - given Offset = Offset(maxLineNumber.toString.length + 2) - - val sb = StringBuilder() - - // Title using the primary position - val posString = posStr(pos1, msg, diagnosticLevel(dia)) - if posString.nonEmpty then sb.append(posString).append(EOL) - - // Display leading text if present - msg.leading.foreach { leadingText => - sb.append(leadingText) - if !leadingText.endsWith(EOL) then sb.append(EOL) - } + val minLine = parts.map(_.srcPos.startLine).min + val maxLine = parts.map(_.srcPos.endLine).max // Render the unified code snippet val startOffset = source.lineToOffset(minLine) @@ -316,6 +290,7 @@ trait MessageRendering { } val lines = linesFrom(syntax) + val maxLineNumber = maxLine + 1 val lineNumberWidth = maxLineNumber.toString.length // Render each line with its markers and messages @@ -329,7 +304,7 @@ trait MessageRendering { sb.append(lnum).append(lineContent.stripLineEnd).append(EOL) // Find all positions that should show markers after this line - val partsOnLine = validParts.filter(_.srcPos.startLine == lineNum) + val partsOnLine = parts.filter(_.srcPos.startLine == lineNum) .sortBy(p => (p.srcPos.startColumn, !p.isPrimary)) if partsOnLine.size == 1 then @@ -382,17 +357,76 @@ trait MessageRendering { connectorLine.append(msgPadding).append(msgText) sb.append(connectorLine).append(EOL) + end renderPartsForFile + + /** Group consecutive parts by their source file. */ + private def groupPartsByFile(parts: List[Message.MessagePart]): List[(SourceFile, List[Message.MessagePart])] = + if parts.isEmpty then Nil + else + val head = parts.head + val source = head.srcPos.source + val (sameSrc, rest) = parts.span(_.srcPos.source == source) + (source, sameSrc) :: groupPartsByFile(rest) + + /** Render a message using multi-span information from Message.parts. */ + def messageAndPosFromParts(dia: Diagnostic)(using Context): String = + val msg = dia.msg + val pos = dia.pos + val pos1 = adjust(pos.nonInlined) + val msgParts = msg.parts + + if msgParts.isEmpty then + return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message + + // Collect all positions from message parts + val validParts = msgParts.filter(p => p.srcPos.exists && p.srcPos.source.file.exists) + + if validParts.isEmpty then + return msg.leading.map(_ + "\n").getOrElse("") + msg.message + + // Group parts by consecutive source files + val groupedParts = groupPartsByFile(validParts) + + // Calculate the maximum line number across all files for consistent offset + val maxLineNumber = validParts.map(_.srcPos.endLine).max + 1 + + given Level = Level(dia.level) + given Offset = Offset(maxLineNumber.toString.length + 2) + + val sb = StringBuilder() + + // Title using the primary position + val posString = posStr(pos1, msg, diagnosticLevel(dia)) + if posString.nonEmpty then sb.append(posString).append(EOL) + + // Display leading text if present + msg.leading.foreach { leadingText => + sb.append(leadingText) + if !leadingText.endsWith(EOL) then sb.append(EOL) + } + + // Track the current file + // When starting, we set it to the file of the diagnostic + var currentFile: SourceFile = pos1.source + + // Render each group of parts + for (source, parts) <- groupedParts do + // Add a file indicator line when switching to a different file + if source != currentFile then + sb.append("... ").append(renderPath(source.file)).append(EOL) + currentFile = source + renderPartsForFile(parts, sb) // Add explanation if needed if Diagnostic.shouldExplain(dia) then - sb.append(EOL).append(newBox()) + sb.append(newBox()) sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)") sb.append(EOL).append(newBox(soft = true)) dia.msg.explanation.split(raw"\R").foreach: line => sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line) sb.append(EOL).append(endBox) else if dia.msg.canExplain then - sb.append(EOL).append(offsetBox) + sb.append(offsetBox) sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`") sb.toString diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala index e337c10b595c..86ce1dda58ab 100644 --- a/compiler/src/dotty/tools/dotc/reporting/messages.scala +++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala @@ -1212,6 +1212,30 @@ extends DeclarationMsg(OverrideErrorID), NoDisambiguation: def explain(using Context) = if canExplain then err.whyNoMatchStr(memberTp, otherTp) else "" + /** Whether the overridden symbol has a valid source position */ + private def otherHasValidPos(using Context): Boolean = + val otherPos = other.sourcePos + otherPos.exists && otherPos.source.file.exists + + override def leading(using Context): Option[String] = + if otherHasValidPos then Some(message) else None + + override def parts(using Context): List[Message.MessagePart] = + if otherHasValidPos then + List( + Message.MessagePart( + i"the overridden ${other.showKind} is here", + other.sourcePos, + isPrimary = false + ), + Message.MessagePart( + i"the overriding ${member.showKind} $core", + member.sourcePos, + isPrimary = true + ) + ) + else Nil + class ForwardReferenceExtendsOverDefinition(value: Symbol, definition: Symbol)(using Context) extends ReferenceMsg(ForwardReferenceExtendsOverDefinitionID) { extension (sym: Symbol) def srcLine = sym.line + 1 diff --git a/tests/neg/override-multi-file-error.check b/tests/neg/override-multi-file-error.check new file mode 100644 index 000000000000..37f1657ff89f --- /dev/null +++ b/tests/neg/override-multi-file-error.check @@ -0,0 +1,13 @@ +-- [E164] Declaration Error: tests/neg/override-multi-file-error/B.scala:2:15 ------------------------------------------ +error overriding method foo in class A of type => Int; + method foo of type => String has incompatible type +... tests/neg/override-multi-file-error/A.scala +2 | def foo: Int = 0 + | - + | the overridden method is here +... tests/neg/override-multi-file-error/B.scala +2 | override def foo: String = "0" // error + | ^ + | the overriding method has incompatible type + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/override-multi-file-error/A.scala b/tests/neg/override-multi-file-error/A.scala new file mode 100644 index 000000000000..84516facb381 --- /dev/null +++ b/tests/neg/override-multi-file-error/A.scala @@ -0,0 +1,3 @@ +class A: + def foo: Int = 0 + diff --git a/tests/neg/override-multi-file-error/B.scala b/tests/neg/override-multi-file-error/B.scala new file mode 100644 index 000000000000..837e8ca5757e --- /dev/null +++ b/tests/neg/override-multi-file-error/B.scala @@ -0,0 +1,3 @@ +class B extends A: + override def foo: String = "0" // error + diff --git a/tests/neg/override-multi-span.check b/tests/neg/override-multi-span.check new file mode 100644 index 000000000000..a967c1139b7d --- /dev/null +++ b/tests/neg/override-multi-span.check @@ -0,0 +1,14 @@ +-- [E164] Declaration Error: tests/neg/override-multi-span.scala:6:15 -------------------------------------------------- +error overriding method foo in class A of type => Int; + method foo of type => String has incompatible type +2 | def foo: Int = 0 + | - + | the overridden method is here +3 |def main(): Unit = +4 | println("Hello") +5 |class B extends A: +6 | override def foo: String = "0" // error + | ^ + | the overriding method has incompatible type + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/override-multi-span.scala b/tests/neg/override-multi-span.scala new file mode 100644 index 000000000000..3250eb5dca49 --- /dev/null +++ b/tests/neg/override-multi-span.scala @@ -0,0 +1,6 @@ +class A: + def foo: Int = 0 +def main(): Unit = + println("Hello") +class B extends A: + override def foo: String = "0" // error From 19ffcb35e7580a1c5df43d90df8dad3ddbab7d2c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 9 Dec 2025 23:35:30 +0100 Subject: [PATCH 16/19] Fix line splitting --- .../src/dotty/tools/dotc/reporting/MessageRendering.scala | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala index b2ddaccbfa95..42a8659c852e 100644 --- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala +++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala @@ -285,8 +285,12 @@ trait MessageRendering { case _ => false } val (line, rest0) = arr.span(!pred(_)) - val (_, rest) = rest0.span(pred) - new String(line) :: { if (rest.isEmpty) Nil else linesFrom(rest) } + // Only consume one line terminator (CRLF counts as one) + val rest = + if rest0.isEmpty then rest0 + else if rest0(0) == CR && rest0.length > 1 && rest0(1) == LF then rest0.drop(2) + else rest0.drop(1) + new String(line) :: { if rest.isEmpty then Nil else linesFrom(rest) } } val lines = linesFrom(syntax) From 4e591de824170d4d213e7e2fe657bde00ba72974 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 9 Dec 2025 23:39:13 +0100 Subject: [PATCH 17/19] Update checkfiles for CC tests --- .../captures/consume-in-constructor.check | 33 ++++++--- .../captures/consume-twice-same-line.check | 6 +- .../captures/consume-twice.check | 2 +- tests/neg-custom-args/captures/i24373.check | 39 +++++++--- tests/neg-custom-args/captures/i24373a.check | 74 ++++++++++++++----- .../captures/lazyListState.check | 20 +++-- tests/neg-custom-args/captures/lazylist.check | 25 ++++++- .../captures/mut-iterator1.check | 12 ++- .../captures/sep-curried-par.check | 13 ++-- .../neg-custom-args/captures/sepchecks5.check | 13 +++- .../captures/unbox-overrides.check | 59 ++++++++++----- .../captures/unscoped-extrude.check | 13 +++- .../captures/unsound-reach-4.check | 17 +++-- 13 files changed, 233 insertions(+), 93 deletions(-) diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check index 4937bf7fc6e4..4fb2a49a8e87 100644 --- a/tests/neg-custom-args/captures/consume-in-constructor.check +++ b/tests/neg-custom-args/captures/consume-in-constructor.check @@ -1,19 +1,32 @@ -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 -------------------------------------------- +Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value b +18 | val a2 = A2(b) + | - + | The capability was consumed here. +19 | val _: A2^{cap, b} = a2 20 | println(b) // error | ^ - |Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2 - |on line 18 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability in the type of value b + | Then, it was used here + -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 -------------------------------------------- +Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2 +and therefore is no longer available. + +where: b is a value in class A1 + b² is a value in method Test + cap is a fresh root capability in the type of value a1 +18 | val a2 = A2(b) + | - + | The capability was consumed here. +19 | val _: A2^{cap, b} = a2 +20 | println(b) // error 21 | println(a1) // error, since `b` was consumed before | ^^ - |Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2 - |on line 18 and therefore is no longer available. - | - |where: b is a value in class A1 - | b² is a value in method Test - | cap is a fresh root capability in the type of value a1 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:27:10 -------------------------------------------- 27 | println(b) // error, b is hidden in the type of a1 | ^ diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check index d549f450be1d..2617e42d538a 100644 --- a/tests/neg-custom-args/captures/consume-twice-same-line.check +++ b/tests/neg-custom-args/captures/consume-twice-same-line.check @@ -1,4 +1,4 @@ --- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 --------------------------------------- +-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 -------------------------------------------- Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. @@ -8,7 +8,7 @@ where: ^ refers to a fresh root capability in the type of parameter x | | Then, it was used here | The capability was consumed here. --- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 --------------------------------------- +-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 -------------------------------------------- Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. @@ -18,7 +18,7 @@ where: ^ refers to a fresh root capability in the type of parameter x | | Then, it was used here | The capability was consumed here. --- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 --------------------------------------- +-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 -------------------------------------------- Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check index 6f88f54a1d4d..1fd11b4f6c83 100644 --- a/tests/neg-custom-args/captures/consume-twice.check +++ b/tests/neg-custom-args/captures/consume-twice.check @@ -1,4 +1,4 @@ --- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 -------------------------------------------------- +-- Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 ------------------------------------------------------- Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send and therefore is no longer available. diff --git a/tests/neg-custom-args/captures/i24373.check b/tests/neg-custom-args/captures/i24373.check index 08e196fc1dc9..497749b42b24 100644 --- a/tests/neg-custom-args/captures/i24373.check +++ b/tests/neg-custom-args/captures/i24373.check @@ -1,21 +1,36 @@ -- Error: tests/neg-custom-args/captures/i24373.scala:28:2 ------------------------------------------------------------- +Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x1 +27 | x1.sink1 + | -- + | The capability was consumed here. 28 | x1.sink1 // error | ^^ - | Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1 - | on line 27 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x1 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373.scala:32:2 ------------------------------------------------------------- +Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x2 +31 | x2.sink2 + | -- + | The capability was consumed here. 32 | x2.sink2 // error | ^^ - | Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2 - | on line 31 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x2 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373.scala:49:8 ------------------------------------------------------------- +Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x6 +48 | sink6(x6) + | -- + | The capability was consumed here. 49 | sink6(x6) // error | ^^ - | Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6 - | on line 48 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x6 + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/i24373a.check b/tests/neg-custom-args/captures/i24373a.check index 61198e8cc676..91a287772378 100644 --- a/tests/neg-custom-args/captures/i24373a.check +++ b/tests/neg-custom-args/captures/i24373a.check @@ -1,38 +1,72 @@ -- Error: tests/neg-custom-args/captures/i24373a.scala:15:8 ------------------------------------------------------------ +Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x1 +13 | sink1(x1) + | -- + | The capability was consumed here. +14 | sink1(x1) // ok, rd/rd 15 | sink2(x1) // error | ^^ - | Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1 - | on line 13 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x1 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373a.scala:19:8 ------------------------------------------------------------ +Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2 +and therefore is no longer available. +18 | sink2(x2) + | -- + | The capability was consumed here. 19 | sink1(x2) // error | ^^ - | Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2 - | on line 18 and therefore is no longer available. + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373a.scala:20:8 ------------------------------------------------------------ +Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x2 +18 | sink2(x2) + | -- + | The capability was consumed here. +19 | sink1(x2) // error 20 | sink2(x2) // error | ^^ - | Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2 - | on line 18 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x2 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373a.scala:25:8 ------------------------------------------------------------ +Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x3 +23 | sink3(x3) + | -- + | The capability was consumed here. +24 | sink3(x3) // ok, rd/rd 25 | sink2(x3) // error | ^^ - | Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3 - | on line 23 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x3 + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373a.scala:29:8 ------------------------------------------------------------ +Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2 +and therefore is no longer available. +28 | sink2(x4) + | -- + | The capability was consumed here. 29 | sink3(x4) // error | ^^ - | Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2 - | on line 28 and therefore is no longer available. + | Then, it was used here + -- Error: tests/neg-custom-args/captures/i24373a.scala:30:8 ------------------------------------------------------------ +Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2 +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of value x4 +28 | sink2(x4) + | -- + | The capability was consumed here. +29 | sink3(x4) // error 30 | sink2(x4) // error | ^^ - | Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2 - | on line 28 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of value x4 + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/lazyListState.check b/tests/neg-custom-args/captures/lazyListState.check index bb84f3d7f006..85a9a92a4c2c 100644 --- a/tests/neg-custom-args/captures/lazyListState.check +++ b/tests/neg-custom-args/captures/lazyListState.check @@ -1,10 +1,20 @@ -- [E164] Declaration Error: tests/neg-custom-args/captures/lazyListState.scala:12:39 ---------------------------------- +error overriding method tail in trait State of type -> LazyListIterable[A]^{cap}; + value tail of type LazyListIterable[A]^ has incompatible type + +where: ^ refers to a fresh root capability in the type of value tail + cap is a root capability associated with the result type of -> LazyListIterable[A²]^² + 5 | def tail: LazyListIterable[A]^ + | - + | the overridden method is here + 6 | + 7 |private object State: + 8 | object Empty extends State[Nothing]: + 9 | def head: Nothing = throw new NoSuchElementException("head of empty lazy list") +10 | def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list") +11 | 12 | final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error | ^ - | error overriding method tail in trait State of type -> LazyListIterable[A]^{cap}; - | value tail of type LazyListIterable[A]^ has incompatible type - | - | where: ^ refers to a fresh root capability in the type of value tail - | cap is a root capability associated with the result type of -> LazyListIterable[A²]^² + | the overriding value has incompatible type | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check index 7dc69e879466..d3aa91bfda97 100644 --- a/tests/neg-custom-args/captures/lazylist.check +++ b/tests/neg-custom-args/captures/lazylist.check @@ -44,11 +44,28 @@ | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ---------------------------------------- +error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing]; + method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type + +where: cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^ + 8 | def tail: LazyList[T] + | - + | the overridden method is here + 9 | +10 | def map[U](f: T => U): LazyList[U]^{f, this} = +11 | if isEmpty then LazyNil +12 | else LazyCons(f(head), () => tail.map(f)) +13 | +14 |class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: +15 | def isEmpty = false +16 | def head = x +17 | def tail = xs() // error +18 | +19 |object LazyNil extends LazyList[Nothing]: +20 | def isEmpty = true +21 | def head = ??? 22 | def tail: LazyList[Nothing]^ = ??? // error overriding | ^ - | error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing]; - | method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type - | - | where: cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^ + | the overriding method has incompatible type | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-iterator1.check b/tests/neg-custom-args/captures/mut-iterator1.check index 2a167a752e41..df630d89a58e 100644 --- a/tests/neg-custom-args/captures/mut-iterator1.check +++ b/tests/neg-custom-args/captures/mut-iterator1.check @@ -1,5 +1,13 @@ -- [E164] Declaration Error: tests/neg-custom-args/captures/mut-iterator1.scala:9:15 ----------------------------------- +error overriding method next in trait Iterator of type (): U; + method next of type (): U is an update method, cannot override a read-only method +5 | def next(): T + | - + | the overridden method is here +6 | +7 | def map[U](f: T => U): Iterator[U] = new Iterator: +8 | def hasNext = Iterator.this.hasNext 9 | update def next() = f(Iterator.this.next()) // error | ^ - | error overriding method next in trait Iterator of type (): U; - | method next of type (): U is an update method, cannot override a read-only method + | the overriding method is an update method, cannot override a read-only method + diff --git a/tests/neg-custom-args/captures/sep-curried-par.check b/tests/neg-custom-args/captures/sep-curried-par.check index 2172c5699fa8..9a526dbd817a 100644 --- a/tests/neg-custom-args/captures/sep-curried-par.check +++ b/tests/neg-custom-args/captures/sep-curried-par.check @@ -34,12 +34,15 @@ |where: => refers to a fresh root capability in the type of value p | =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 --------------------------------------------------- +Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried +and therefore is no longer available. + +where: => refers to a fresh root capability in the type of value p 18 | parCurried(p)(p) // error: consume failure - | ^ - |Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried - |on line 18 and therefore is no longer available. - | - |where: => refers to a fresh root capability in the type of value p + | - ^ + | | Then, it was used here + | The capability was consumed here. + -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ---------------------------------------------------- 21 | foo(c)(c) // error: separation | ^ diff --git a/tests/neg-custom-args/captures/sepchecks5.check b/tests/neg-custom-args/captures/sepchecks5.check index ab7ae86a9cef..b250185c7657 100644 --- a/tests/neg-custom-args/captures/sepchecks5.check +++ b/tests/neg-custom-args/captures/sepchecks5.check @@ -9,9 +9,14 @@ | Separation failure: argument to consume parameter with type (io : Object^) refers to parameter io. | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 -------------------------------------------------------- +Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g +and therefore is no longer available. + +where: ^ refers to a fresh root capability in the type of parameter io +19 | val f2 = g(io) // error + | -- + | The capability was consumed here. 20 | par(f2)(() => println(io)) // error | ^^ - | Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g - | on line 19 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability in the type of parameter io + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check index 883ab56c59a5..6e13df9bcd1d 100644 --- a/tests/neg-custom-args/captures/unbox-overrides.check +++ b/tests/neg-custom-args/captures/unbox-overrides.check @@ -1,30 +1,55 @@ -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ---------------------------------- +error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; + method foo of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition + +where: ^ refers to a fresh root capability in the type of type C² + ^² refers to a fresh root capability in the type of type C³ +4 | def foo[@reserve C^]: Object^{C} + | - + | the overridden method is here +5 | def bar[C^]: Object^{C} +6 | +7 |trait B extends A: 8 | def foo[C^]: Object^{C} // error | ^ - |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; - | method foo of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition - | - |where: ^ refers to a fresh root capability in the type of type C² - | ^² refers to a fresh root capability in the type of type C³ + |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:9:6 ---------------------------------- +error overriding method bar in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; + method bar of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition + +where: ^ refers to a fresh root capability in the type of type C² + ^² refers to a fresh root capability in the type of type C³ +5 | def bar[C^]: Object^{C} + | - + | the overridden method is here +6 | +7 |trait B extends A: +8 | def foo[C^]: Object^{C} // error 9 | def bar[@reserve C^]: Object^{C} // error | ^ - |error overriding method bar in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; - | method bar of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition - | - |where: ^ refers to a fresh root capability in the type of type C² - | ^² refers to a fresh root capability in the type of type C³ + |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:15:15 -------------------------------- -15 |abstract class C extends A, B2 // error - | ^ - |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; - | method foo in trait B2 of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition - | - |where: ^ refers to a fresh root capability in the type of type C² - | ^² refers to a fresh root capability in the type of type C³ +error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C}; + method foo in trait B2 of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition + +where: ^ refers to a fresh root capability in the type of type C² + ^² refers to a fresh root capability in the type of type C³ + 4 | def foo[@reserve C^]: Object^{C} + | - + | the overridden method is here + 5 | def bar[C^]: Object^{C} + 6 | + 7 |trait B extends A: + 8 | def foo[C^]: Object^{C} // error + 9 | def bar[@reserve C^]: Object^{C} // error +10 | +11 |trait B2: +12 | def foo[C^]: Object^{C} + | ^ + |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unscoped-extrude.check b/tests/neg-custom-args/captures/unscoped-extrude.check index b59c6bc2fb48..4f6b47dabe1c 100644 --- a/tests/neg-custom-args/captures/unscoped-extrude.check +++ b/tests/neg-custom-args/captures/unscoped-extrude.check @@ -1,7 +1,12 @@ -- Error: tests/neg-custom-args/captures/unscoped-extrude.scala:13:4 --------------------------------------------------- +Separation failure: Illegal access to (r : Ref[String]^), which was consumed in an assignment to variable x +and therefore is no longer available. + +where: ^ refers to a fresh root capability classified as Unscoped in the type of value r +12 | x = r // should be consumed here + | ----- + | The capability was consumed here. 13 | r // error | ^ - | Separation failure: Illegal access to (r : Ref[String]^), which was consumed in an assignment to variable x - | on line 12 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability classified as Unscoped in the type of value r + | Then, it was used here + diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index 6e4271cf0057..3ec2529eac5d 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -19,13 +19,18 @@ | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 --------------------------------- +error overriding method use in trait Foo of type (x: File^): File^²; + method use of type (@consume x: File^): File^³ has incompatible type + +where: ^ refers to the universal root capability + ^² refers to a fresh root capability created in class Bar + ^³ refers to a root capability associated with the result type of (@consume x: File^): File^³ +15 | def use(x: F): X + | - + | the overridden method is here +16 |class Bar extends Foo[File^]: // error 17 | def use(consume x: F): File^ = x // error consume override | ^ - | error overriding method use in trait Foo of type (x: File^): File^²; - | method use of type (@consume x: File^): File^³ has incompatible type - | - | where: ^ refers to the universal root capability - | ^² refers to a fresh root capability created in class Bar - | ^³ refers to a root capability associated with the result type of (@consume x: File^): File^³ + | the overriding method has incompatible type | | longer explanation available when compiling with `-explain` From 0bcade9d7e47802429daeabfbe1b5d144a3e5db1 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 10 Dec 2025 00:15:21 +0100 Subject: [PATCH 18/19] Update checkfiles for overriding errors --- tests/neg/abstract-givens.check | 31 +++++++++++--- tests/neg/exports2.check | 11 ++++- tests/neg/harmonize.scala | 4 +- tests/neg/i14415.check | 16 +++++-- tests/neg/i23474.check | 17 +++++++- tests/neg/override-scala2-macro.check | 15 +++++-- tests/neg/parent-refinement-access.check | 16 ++++--- tests/neg/publicInBinaryOverride.check | 12 +++++- tests/neg/targetName-override.check | 54 +++++++++++++++++++++--- tests/warn/matchable.scala | 2 +- 10 files changed, 143 insertions(+), 35 deletions(-) diff --git a/tests/neg/abstract-givens.check b/tests/neg/abstract-givens.check index 51f50db266c2..e02a980d5ad0 100644 --- a/tests/neg/abstract-givens.check +++ b/tests/neg/abstract-givens.check @@ -3,17 +3,34 @@ | ^ |instance cannot be created, since def iterator: Iterator[A] in trait IterableOnce in package scala.collection is not defined -- [E164] Declaration Error: tests/neg/abstract-givens.scala:8:8 ------------------------------------------------------- +error overriding given instance y in trait T of type (using x$1: Int): String; + given instance y of type (using x$1: Int): String cannot override final member given instance y in trait T +3 | given y(using Int): String = summon[Int].toString + | - + | the overridden given instance is here +4 | given z[T](using T): List[T] +5 | +6 |object Test extends T: +7 | given x: Int = 22 8 | given y(using Int): String = summon[Int].toString * 22 // error | ^ - | error overriding given instance y in trait T of type (using x$1: Int): String; - | given instance y of type (using x$1: Int): String cannot override final member given instance y in trait T + | the overriding given instance cannot override final member given instance y in trait T + -- [E164] Declaration Error: tests/neg/abstract-givens.scala:9:8 ------------------------------------------------------- +error overriding given instance z in trait T² of type [T](using x$1: T): List[T]; + given instance z of type [T](using x$1: T): Seq[T] has incompatible type + +where: T is a type variable + T² is a trait in the empty package +4 | given z[T](using T): List[T] + | - + | the overridden given instance is here +5 | +6 |object Test extends T: +7 | given x: Int = 22 +8 | given y(using Int): String = summon[Int].toString * 22 // error 9 | given z[T](using T): Seq[T] = List(summon[T]) // error | ^ - | error overriding given instance z in trait T² of type [T](using x$1: T): List[T]; - | given instance z of type [T](using x$1: T): Seq[T] has incompatible type - | - | where: T is a type variable - | T² is a trait in the empty package + | the overriding given instance has incompatible type | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/exports2.check b/tests/neg/exports2.check index 245538b12abb..f5c096bdd3da 100644 --- a/tests/neg/exports2.check +++ b/tests/neg/exports2.check @@ -1,5 +1,12 @@ -- [E164] Declaration Error: tests/neg/exports2.scala:8:11 ------------------------------------------------------------- +error overriding method f in trait B of type => String; + method f of type => String cannot override since it comes from an export +5 | def f: String = "abc" + | - + | the overridden method is here +6 | +7 |object C extends B: 8 | export A._ // error | ^ - | error overriding method f in trait B of type => String; - | method f of type => String cannot override since it comes from an export + | the overriding method cannot override since it comes from an export + diff --git a/tests/neg/harmonize.scala b/tests/neg/harmonize.scala index 72275a8f68fc..aa60656f0278 100644 --- a/tests/neg/harmonize.scala +++ b/tests/neg/harmonize.scala @@ -79,9 +79,9 @@ object Test { val a4 = ArrayBuffer(1.0f, 1L) val b4: ArrayBuffer[Double] = a4 // error: no widening val a5 = ArrayBuffer(1.0f, 1L, f()) - val b5: ArrayBuffer[Float | Long | Int] = a5 + val b5: ArrayBuffer[Float | Long | Int] = a5 // error: no widening val a6 = ArrayBuffer(1.0f, 1234567890) - val b6: ArrayBuffer[Float | Int] = a6 + val b6: ArrayBuffer[Float | Int] = a6 // error: no widening def totalDuration(results: List[Long], cond: Boolean): Long = results.map(r => if (cond) r else 0).sum diff --git a/tests/neg/i14415.check b/tests/neg/i14415.check index 596debf175dc..70cb321079c1 100644 --- a/tests/neg/i14415.check +++ b/tests/neg/i14415.check @@ -1,5 +1,13 @@ -- [E164] Declaration Error: tests/neg/i14415.scala:21:6 --------------------------------------------------------------- -21 |class X extends E with D // error - | ^ - | error overriding method m in trait C of type (a: Int): Int; - | method m in trait D of type (a: Int): Int needs `abstract override` modifiers +error overriding method m in trait C of type (a: Int): Int; + method m in trait D of type (a: Int): Int needs `abstract override` modifiers +10 | abstract override def m(a:Int):Int = { return super.m(a); } + | - + | the overridden method is here +11 |} +12 | +13 |trait D extends B with C { +14 | override def m(a:Int):Int = { return super.m(a); } + | ^ + | the overriding method needs `abstract override` modifiers + diff --git a/tests/neg/i23474.check b/tests/neg/i23474.check index 441978be6809..2612e09c808f 100644 --- a/tests/neg/i23474.check +++ b/tests/neg/i23474.check @@ -9,10 +9,23 @@ | class Z needs to be abstract, since var comment_=(x$1: String): Unit in trait Comment is not defined | (Note that an abstract var requires a setter in addition to the getter) -- [E164] Declaration Error: tests/neg/i23474.scala:11:15 -------------------------------------------------------------- +error overriding variable comment in trait Comment of type String; + method comment of type => String cannot override a mutable variable + 2 | var comment: String + | - + | the overridden variable is here + 3 |} + 4 | + 5 |case class Y(val comment: String) extends Comment // error + 6 | + 7 |class Z extends Comment: // error + 8 | val comment: String = "" + 9 | +10 |class X extends Comment: // error 11 | override def comment: String = "" // error | ^ - | error overriding variable comment in trait Comment of type String; - | method comment of type => String cannot override a mutable variable + | the overriding method cannot override a mutable variable + -- Error: tests/neg/i23474.scala:10:6 ---------------------------------------------------------------------------------- 10 |class X extends Comment: // error | ^ diff --git a/tests/neg/override-scala2-macro.check b/tests/neg/override-scala2-macro.check index ff5e478342dd..9014bdb9ac82 100644 --- a/tests/neg/override-scala2-macro.check +++ b/tests/neg/override-scala2-macro.check @@ -1,5 +1,12 @@ -- [E164] Declaration Error: tests/neg/override-scala2-macro.scala:2:22 ------------------------------------------------ -2 | override inline def f[A >: Any](args: A*): String = ??? // error - | ^ - |error overriding method f in class StringContext of type [A >: Any](args: Seq[A]): String; - | method f of type [A >: Any](args: Seq[A]): String cannot be used here - only Scala-2 macros can override Scala-2 macros +error overriding method f in class StringContext of type [A >: Any](args: Seq[A]): String; + method f of type [A >: Any](args: Seq[A]): String cannot be used here - only Scala-2 macros can override Scala-2 macros +... library/src/scala/StringContext.scala +197 | def f[A >: Any](args: A*): String = macro ??? // fasttracked to scala.tools.reflect.FormatInterpolator::interpolateF + | - + | the overridden method is here +... tests/neg/override-scala2-macro.scala + 2 | override inline def f[A >: Any](args: A*): String = ??? // error + | ^ + | the overriding method cannot be used here - only Scala-2 macros can override Scala-2 macros + diff --git a/tests/neg/parent-refinement-access.check b/tests/neg/parent-refinement-access.check index 5cde9d51558f..3ecb0292f726 100644 --- a/tests/neg/parent-refinement-access.check +++ b/tests/neg/parent-refinement-access.check @@ -1,7 +1,13 @@ -- [E164] Declaration Error: tests/neg/parent-refinement-access.scala:6:6 ---------------------------------------------- +error overriding value x in trait Year2 of type Int; + value x in trait Gen of type Any has weaker access privileges; it should be public +(Note that value x in trait Year2 of type Int is abstract, +and is therefore overridden by concrete value x in trait Gen of type Any) +4 | private[Gen] val x: Any = () + | ^ + | the overriding value has weaker access privileges; it should be public +5 | 6 |trait Year2(private[Year2] val value: Int) extends (Gen { val x: Int }) // error - | ^ - | error overriding value x in trait Year2 of type Int; - | value x in trait Gen of type Any has weaker access privileges; it should be public - | (Note that value x in trait Year2 of type Int is abstract, - | and is therefore overridden by concrete value x in trait Gen of type Any) + | - + | the overridden value is here + diff --git a/tests/neg/publicInBinaryOverride.check b/tests/neg/publicInBinaryOverride.check index e44692c78525..e90624af18de 100644 --- a/tests/neg/publicInBinaryOverride.check +++ b/tests/neg/publicInBinaryOverride.check @@ -1,5 +1,13 @@ -- [E164] Declaration Error: tests/neg/publicInBinaryOverride.scala:8:15 ----------------------------------------------- +error overriding method f in class A of type (): Unit; + method f of type (): Unit also needs to be declared with @publicInBinary +4 | @publicInBinary def f(): Unit = () + | - + | the overridden method is here +5 | @publicInBinary def g(): Unit = () +6 | +7 |class B extends A: 8 | override def f(): Unit = () // error | ^ - | error overriding method f in class A of type (): Unit; - | method f of type (): Unit also needs to be declared with @publicInBinary + | the overriding method also needs to be declared with @publicInBinary + diff --git a/tests/neg/targetName-override.check b/tests/neg/targetName-override.check index 230b7fe77745..9e1b1e7542bf 100644 --- a/tests/neg/targetName-override.check +++ b/tests/neg/targetName-override.check @@ -1,18 +1,60 @@ -- [E164] Declaration Error: tests/neg/targetName-override.scala:16:35 ------------------------------------------------- +error overriding method foo in class Alpha of type (): Int; + method foo of type (): Int should not have a @targetName annotation since the overridden member hasn't one either + 6 | def foo() = 1 + | - + | the overridden method is here + 7 | + 8 | @targetName("foo1") def foo(x: T): T + 9 | +10 | @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this +11 | +12 |} +13 | +14 |class Beta extends Alpha[String] { // error: needs to be abstract +15 | 16 | @targetName("foo1") override def foo() = 1 // error: should not have a target name | ^ - |error overriding method foo in class Alpha of type (): Int; - | method foo of type (): Int should not have a @targetName annotation since the overridden member hasn't one either + | the overriding method should not have a @targetName annotation since the overridden member hasn't one either + -- [E164] Declaration Error: tests/neg/targetName-override.scala:18:25 ------------------------------------------------- +error overriding method foo in class Alpha of type (x: String): String; + method foo of type (x: String): String has a different target name annotation; it should be @targetName(foo1) + 8 | @targetName("foo1") def foo(x: T): T + | - + | the overridden method is here + 9 | +10 | @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this +11 | +12 |} +13 | +14 |class Beta extends Alpha[String] { // error: needs to be abstract +15 | +16 | @targetName("foo1") override def foo() = 1 // error: should not have a target name +17 | 18 | @targetName("baz") def foo(x: String): String = x ++ x // error: has a different target name annotation | ^ - | error overriding method foo in class Alpha of type (x: String): String; - | method foo of type (x: String): String has a different target name annotation; it should be @targetName(foo1) + | the overriding method has a different target name annotation; it should be @targetName(foo1) + -- [E164] Declaration Error: tests/neg/targetName-override.scala:20:15 ------------------------------------------------- +error overriding method ++ in class Alpha of type (xs: Alpha[String]): Alpha[String]; + method ++ of type (xs: Alpha[String]): Alpha[String] misses a target name annotation @targetName(append) +10 | @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this + | - + | the overridden method is here +11 | +12 |} +13 | +14 |class Beta extends Alpha[String] { // error: needs to be abstract +15 | +16 | @targetName("foo1") override def foo() = 1 // error: should not have a target name +17 | +18 | @targetName("baz") def foo(x: String): String = x ++ x // error: has a different target name annotation +19 | 20 | override def ++ (xs: Alpha[String]): Alpha[String] = this // error: misses a targetname annotation | ^ - | error overriding method ++ in class Alpha of type (xs: Alpha[String]): Alpha[String]; - | method ++ of type (xs: Alpha[String]): Alpha[String] misses a target name annotation @targetName(append) + | the overriding method misses a target name annotation @targetName(append) + -- Error: tests/neg/targetName-override.scala:14:6 --------------------------------------------------------------------- 14 |class Beta extends Alpha[String] { // error: needs to be abstract | ^^^^ diff --git a/tests/warn/matchable.scala b/tests/warn/matchable.scala index 8adcdcf1c90a..2a27ad36428c 100644 --- a/tests/warn/matchable.scala +++ b/tests/warn/matchable.scala @@ -13,7 +13,7 @@ def foo[T](x: T): Matchable = List(x) match case (x: Int) :: Nil => // warn: should not be scrutinized println("int") - x + x // warn case List(x: String) => // warn: should not be scrutinized println("string") x From fddee364ff17f2048550f10ab18fc8b8e4b60476 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 10 Dec 2025 14:05:17 +0100 Subject: [PATCH 19/19] Resolve rebase conflicts --- .../captures/linear-buffer-2.check | 36 +++---------------- .../captures/linear-buffer.check | 36 +++---------------- .../captures/sep-consume.check | 18 ++-------- 3 files changed, 10 insertions(+), 80 deletions(-) diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 67dbff6bd419..1e997ba87366 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -2,47 +2,33 @@ Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of parameter buf +where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf 11 | val buf1: Buffer[Int]^ = buf.append(1) | --- | The capability was consumed here. 12 | val buf2 = buf1.append(2) // OK 13 | val buf3 = buf.append(3) // error | ^^^ -<<<<<<< HEAD - | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append - | on line 11 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 18 | if ??? then buf1.append(2) // OK | ---- | The capability was consumed here. 19 | else buf1.append(3) // OK 20 | val buf3 = buf1.append(4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append - |on line 18 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 25 | case 1 => buf1.append(2) // OK | ---- | The capability was consumed here. @@ -50,20 +36,13 @@ where: ^ refers to a fresh root capability in the type of value buf1 27 | case _ => buf1.append(3) 28 | val buf3 = buf1.append(4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append - |on line 25 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 33 | case 1 => buf1.append(2) // OK | ---- | The capability was consumed here. @@ -73,15 +52,8 @@ where: ^ refers to a fresh root capability in the type of value buf1 37 | case 5 => buf1.append(5) 38 | val buf3 = buf1.append(4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append - |on line 33 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(1) // error | ^^^ diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index b0c90a038e15..9ec4ca0c8089 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -37,47 +37,33 @@ Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of parameter buf +where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf 21 | val buf1: Buffer[Int]^ = app(buf, 1) | --- | The capability was consumed here. 22 | val buf2 = app(buf1, 2) // OK 23 | val buf3 = app(buf, 3) // error | ^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app - |on line 21 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 ----------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 28 | if ??? then app(buf1, 2) // OK | ---- | The capability was consumed here. 29 | else app(buf1, 3) // OK 30 | val buf3 = app(buf1, 4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app - |on line 28 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 ----------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 35 | case 1 => app(buf1, 2) // OK | ---- | The capability was consumed here. @@ -85,20 +71,13 @@ where: ^ refers to a fresh root capability in the type of value buf1 37 | case _ => app(buf1, 3) 38 | val buf3 = app(buf1, 4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app - |on line 35 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 ----------------------------------------------------- Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of value buf1 +where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 43 | case 1 => app(buf1, 2) // OK | ---- | The capability was consumed here. @@ -108,15 +87,8 @@ where: ^ refers to a fresh root capability in the type of value buf1 47 | case 5 => app(buf1, 5) 48 | val buf3 = app(buf1, 4) // error | ^^^^ -<<<<<<< HEAD - |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app - |on line 43 and therefore is no longer available. - | - |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------ 52 | app(buf, 1) // error | ^^^ diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 40e1643c8455..d3f1b3086694 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -7,26 +7,19 @@ Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of parameter x +where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x 18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap` | - | The capability was consumed here. 19 | x.put(42) // error | ^ -<<<<<<< HEAD - | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad - | on line 18 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad and therefore is no longer available. -where: ^ refers to a fresh root capability in the type of parameter x +where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x 18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap` | - | The capability was consumed here. @@ -34,15 +27,8 @@ where: ^ refers to a fresh root capability in the type of parameter x 20 | x.get // ok rd/rd 21 | par(rx, () => x.put(42)) // error | ^ -<<<<<<< HEAD - | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad - | on line 18 and therefore is no longer available. - | - | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x -======= | Then, it was used here ->>>>>>> 2ee70f2604 (Update checkfiles) -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^