VerifyError: erased context function parameter before non-erased produces invalid bytecode

[haskiindahouse]

Compiler version

3.8.3 (also verified on 3.7.3 and 3.6.4)

Minimized code

import scala.language.experimental.erasedDefinitions

class Proof
erased given Proof = Proof()

def mixed: (erased Proof) ?=> Int ?=> String =
  s"value: ${summon[Int]}"

@main def test(): Unit =
  given Int = 99
  println(mixed)

Output (click arrow to expand)

Details

Exception in thread "main" java.lang.VerifyError: Bad local variable type
Exception Details:
  Location:
    bug003$package$.mixed(I)Ljava/lang/String; @0: iload_2
  Reason:
    Type top (current frame, locals[2]) is not assignable to integer
  Current Frame:
    bci: @0
    flags: { }
    locals: { 'bug003$package$', integer }
    stack: { }
  Bytecode:
    0000000: 1cba 002e 0000 b0

	at test.main(bug003.scala:10)

Expectation

Should print value: 99.

The method signature is mixed(I)String — one int parameter. But the bytecode uses iload_2 (slot 2) when only slots 0 (this) and 1 (Int) exist. The erased Proof parameter was removed from the signature but slot numbering in the body was not adjusted.

Key observation: order matters

// CRASHES: erased first, then non-erased
def mixed: (erased Proof) ?=> Int ?=> String = s"${summon[Int]}"

// WORKS: non-erased first, then erased (erased in last position)
def reversed: Int ?=> (erased Proof) ?=> String = s"${summon[Int]}"

All these also crash:

def varA: (erased P1) ?=> (erased P2) ?=> Int ?=> String = ...  // 2 erased before non-erased
def varB: (erased P1) ?=> Int ?=> (erased P2) ?=> String = ...  // erased, non-erased, erased
def varC: Int ?=> (erased P1) ?=> String ?=> String = ...       // non-erased, erased, non-erased

The bug triggers whenever an erased context function param appears BEFORE any subsequent non-erased param. Only erased in the very last position is safe.

Notes

• Compiles without errors — the bug is only visible at runtime via JVM bytecode verifier.
• -Ycheck:all passes ALL compiler phases (including genBCode) without detecting the issue.
• inline methods avoid the bug (erased removed during inlining, before bytecode gen).
• Related to java.lang.VerifyError with erased value #16943 (erased VerifyError for regular methods, fixed in Add regression test #17047) — but that fix didn't cover chained context function types.
• Found using my Scala 3 grammar model and DepTyCheck
  Also found via my tools: Recursive macro splice causes StackOverflowError during inlining phase #25724, Duplicate enum name (simple + parametric) causes assertion failure #25723, Parser crash (AssertionError) when line comment hides then in for-generator inside new argument #25248, Crash: AssertionError in TypeOps.dominators with complex context bounds and quoted expression #25246, Crash in tpd.singleton on PreviousErrorType during error recovery (inline match + quoted pattern with unresolved import) #25244

[tanishiking]

For normal parameters, erased parameters are removed from the tree during erasure.

def direct(using erased p: Proof, x: Int): String =
  "value: " + x

// [[syntax trees at end of erasure]]
def direct(using x: Int): String =
  "value: " + Int.box(x)

However, for erased parameters coming from a context-function(?), the erased parameter incorrectly remains in the tree after erasure.

def mixed: (erased Proof) ?=> Int ?=> String =
  s"value: ${summon[Int]}"

// [[syntax trees at end of erasure]]
// the erased parameter incorrectly remains
def mixed(using x$1: Proof, contextual$1: Int): String =
  "value: " + Int.box(contextual$1)

Therefore, the backend assigns local variable slots as if erased parameters were still there:

• 0 = this
• 1 = x$1
• 2 = contextual$1

As a result, the reference to contextual$1 is compiled as iload_2.

On the other hand, the method type stored in methSymbol.info is erased correctly. In TypeErasure, erased parameters are dropped from the MethodType here:

scala3/compiler/src/dotty/tools/dotc/core/TypeErasure.scala

Lines 836 to 844 in 9c90195

	case tp: MethodType =>
	def paramErasure(tpToErase: Type) =
	erasureFn(sourceLanguage, semiEraseVCs, isConstructor, isSymbol, inSigName = false)(tpToErase)
	val (names, formals0) = if tp.hasErasedParams then
	tp.paramNames
	.zip(tp.paramInfos)
	.zip(tp.paramErasureStatuses)
	.collect{ case (param, isErased) if !isErased => param }
	.unzip

So the erased signature of mixed becomes (using Int)String, and the backend builds the JVM descriptor (I)Ljava/lang/String; from that type information

scala3/compiler/src/dotty/tools/backend/jvm/CoreBTypes.scala

Line 144 in 9c90195

MethodBType(msym.info.firstParamTypes.map(toTypeKind), resT)

---

So, the bug is the mismatch between the type and the tree after erasure:

• info correctly drops the erased parameter
• vparams in the erased tree still contains it

That mismatch is what eventually produces the verifier error 👀

---

reversed has the same tree-side problem, but it does not fail because the Int parameter still ends up in slot 1, which matches the erased JVM signature:

def reversed: Int ?=> (erased Proof) ?=> String =
  s"${summon[Int]}"

// [[syntax trees at end of erasure]]
// the erased parameter incorrectly remains
def reversed(using contextual$2: Int, x$1: Proof): String =
  "value: " + Int.box(contextual$2)

So reversed is not actually correct either; it just happens not to trigger invalid bytecode, because the accessed non-erased parameter is still in the expected slot.

Not sure about the case def varC: Int ?=> (erased P1) ?=> String ?=> String = ... // non-erased, erased, non-erased, maybe it access summon[String] in body?