Wrong (not in scope) type argument inserted, leading to ClassCastException

[radeusgd]

Minimized code

object Bug {
  sealed trait Container { s =>
    type A
    def visit[R](int: IntV & s.type => R, str: StrV & s.type => R): R
  }
  final class IntV extends Container { s =>
    type A = Int
    val i: Int = 42
    def visit[R](int: IntV & s.type => R, str: StrV & s.type => R): R = int(this)
  }
  final class StrV extends Container { s =>
    type A = String
    val t: String = "hello"
    def visit[R](int: IntV & s.type => R, str: StrV & s.type => R): R = str(this)
  }

  def minimalOk[R](c: Container { type A = R }): R = c.visit[R](
    int = vi => vi.i : vi.A,
    str = vs => vs.t : vs.A
  )
  def minimalFail[R](c: Container { type A = R }): R = c.visit(
    int = vi => vi.i : vi.A,
    str = vs => vs.t : vs.A
  )

  def main(args: Array[String]): Unit = {
    val e: Container { type A = String } = new StrV
    println(minimalOk(e)) // this one prints "hello"
    println(minimalFail(e)) // this one fails with ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer
  }
}

// in REPL add Bug.main(Array())

Output

The program crashes on the second invocation with a ClassCastException.

hello
Exception in thread "main" java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer (java.lang.String and java.lang.Integer are in module java.base of loader 'bootstrap')
	at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)
	at Bug$.minimalFail$$anonfun$2(bug.scala:23)
	at Bug$StrV.visit(bug.scala:14)
	at Bug$.minimalFail(bug.scala:23)
	at Bug$.main(bug.scala:29)
	at Bug.main(bug.scala)

Expectation

The program should print "hello" twice.
(Other possible outcome, minimalFail may not compile not being able to infer the type to insert into visit).

Analysis

When running dotc with -Xprint:typer one can see that in the case of minimalFail a wrong type parameter is inserted:

def minimalOk[R >: Nothing <: Any](
      c: 
        Bug.Container 
          {
            type A = R
          }
    ): R = 
      c.visit[R](
        int = 
          {
            def $anonfun(vi: Bug.IntV & (c : Bug.Container{A = R})): R = 
              vi.i:vi.A
            closure($anonfun)
          }
      , 
        str = 
          {
            def $anonfun(vs: Bug.StrV & (c : Bug.Container{A = R})): R = 
              vs.t:vs.A
            closure($anonfun)
          }
      )
    def minimalFail[R >: Nothing <: Any](
      c: 
        Bug.Container 
          {
            type A = R
          }
    ): R = 
      c.visit[vi.A](
        int = 
          {
            def $anonfun(vi: Bug.IntV & (c : Bug.Container{A = R})): vi.A = 
              vi.i:vi.A
            closure($anonfun)
          }
      , 
        str = 
          {
            def $anonfun(vs: Bug.StrV & (c : Bug.Container{A = R})): vi.A = 
              vs.t:vs.A
            closure($anonfun)
          }
      )

We can see that in minimalFail case, visit is called with a type parameter vi.A which is not even in scope at the time (it is an argument of a lambda that will follow).
As this argument is not in scope, we don't know if vi could have been correctly instantiated, thus we get the unsound type judgement c.A =:= vi.A =:= Int which is broken when we call minimalFail with a StrV value, because there we have c.A =:= String, leading to String =:= Int and a runtime error.

[smarter]

The code that is supposed to prevent this by removing parameter types from the result type is at https://github.com/lampepfl/dotty/blob/d1185c3b6a31e86f724d2e1ac43b882a452ba2fa/compiler/src/dotty/tools/dotc/typer/Namer.scala#L1499-L1506 (specifically, the avoid call). First thing to do would be to check if this code is actually called here, and if the type variable R has already been constrained to be a supertype of vi.A by this point.