Polymorphic annotations can leak type parameters

[Sporarum]

Compiler version

3.3.1-RC1 (on current main)

Minimized code

Command:
run path/to/file.scala -Xprint:typer

File:

import scala.annotation.Annotation

class myAnnot[T]() extends Annotation

trait Tensor[T]:

  def add: Tensor[T] @myAnnot[T]()


class TensorImpl[A]() extends Tensor[A]:
  def add = this

See also example below without subtyping or inference

Output

[[syntax trees at end of                     typer]] // path/to/file.scala
package <empty> {
  import scala.annotation.Annotation
  class myAnnot[T >: Nothing <: Any]() extends scala.annotation.Annotation() {
    T
  }
  trait Tensor[T >: Nothing <: Any]() extends Object {
    T
    def add: Tensor[Tensor.this.T] @myAnnot[T]
  }
  class TensorImpl[A >: Nothing <: Any]() extends Object(), Tensor[
    TensorImpl.this.A] {
    A
    def add: Tensor[A] @myAnnot[T] = this // This T refers to the parent trait's T !
  }
}

Expectation

[[syntax trees at end of                     typer]] // path/to/file.scala
package <empty> {
  import scala.annotation.Annotation
  class myAnnot[T >: Nothing <: Any]() extends scala.annotation.Annotation() {
    T
  }
  trait Tensor[T >: Nothing <: Any]() extends Object {
    T
    def add: Tensor[Tensor.this.T] @myAnnot[T]
  }
  class TensorImpl[A >: Nothing <: Any]() extends Object(), Tensor[
    TensorImpl.this.A] {
    A
    def add: Tensor[A] @myAnnot[A] = this // Only change
  }
}

[odersky]

Good point. Maybe we should automatically erase all annotations in inferred types? I don't see a feasible way to ensure they are always sound and make sense.

[Sporarum]

For the purpose of qualified types, we really want to keep the annotations

Is it safe to remove the capture set for cc ?

Outside of these two, it's not clear to me what purpose type annotation serve and thus I don't see what harm would be done in erasing them

[Sporarum]

*For qualified types, as long as we are using annotations and not a "real" tree, we really want subclasses to have Tensor[A] @refined[A](...)

[odersky]

For cc we remove all annotations in inferred types and then we re-compute them,

[Sporarum]

I see, I think we have to do that as well, even for other reasons

I'll ask on the scala discord what are the uses of type-parametrised annotations

[Sporarum]

This is actually more general:

class myAnnot[A] extends scala.annotation.Annotation

def foo[T](y: T @myAnnot[T]): T @myAnnot[T] = ???

val s: String = foo[Int](4) // Found:  Int @myAnnot[T]  Required: String

It seems annotations are not traversed at all by the type replacer !

You'll note there was no inference in this example

[Sporarum]

Could we always traverse annotations with every phase ?
(There is a similar issue with inlining)

This seems like it would make them semantically clearer

[odersky]

I fear this would cause a lot of problems, but don't have a concrete counter example.