Typing of the method ignores knowledge that could be collected from type bounds on method targs

[DarkDimius]

trait A {
  type T1
  type T2
  def foo[B <: T1 >: T2] = ... // is T2 <:< T1 in method?
}

As in order to call method foo one needs to verify type bounds, it seems safe for me to assume T2 <:< T1 in the body of the method

This is needed for some compiler rewritings to be type-safe. Eg, specialization of a

class Foo[+A] {
  def bop[@specialized B >: A]: Foo[B] = this
}

will yield

  def bop_sp[@specialized B >: A <: Int & Any]: Foo[B] = this

Without typer knowing that Foo$A is subtype of Int in this example, specialization needs to insert casts.
Unfortunately, for the scheme to be complete, specialization needs to insert casts in every place where we have a source of expected type: arguments of methods, vals, defs. Otherwise the tree does not typecheck.

[DarkDimius]

ping @odersky @adriaanm @smarter @samuelgruetter @namin

Handling this case seems to account for 90% of problems with specialization that we have seen so far.

[samuelgruetter]

So in the body of def bop_sp[@specialized B >: A & Int <: Int & Any]: Foo[B], you want to have the knowledge that A <: Int, and you think that

A & Int <: Int & Any   ==>   A <: Int

The problem is that the above implication does not hold, because A & Int <: Int & Any could have been derived from Int <: Int & Any, which could have been derived from Int <: Int ∧ Int <: Any.

Note: This is (at least slightly) related to #525, where we see that dotty checks that the lower bound of a type parameter always is a subtype of the upper bound.

[DarkDimius]

So in the body of def bop_sp[@specialized B >: A & Int <: Int & Any]: Foo[B], you want to have the knowledge that A <: Int, and you think that

A & Int <: Int & Any   ==>   A <: Int

@samuelgruetter , I had an error in my original text. Please see the update.

def bop_sp[@specialized B >: A <: Int & Any]: Foo[B]

[samuelgruetter]

Do you want to the return type to be Foo[B] or Foo[Int]?

Return type Foo[B] works in scalac:

class Foo[+A] {
  def bop_sp[B >: A <: Int]: Foo[B] = this
}

(but not in dotty because of #525).

[DarkDimius]

It's not only about return type of the method itself, that's about any expected type in general, be it type of val defined in method, or be it argument of a another method called in this one.
https://github.com/AlexSikia/dotty/blob/a9ebb46e9e0cd2d2cbd9c2a8757db1fc1b9f802a/tests/pos/specialization/this_specialization.scala#L3-L8 has some examples

[DarkDimius]

And yes, in this example, for the body of method to typecheck, I need it to be able to infer that F[A] is a subtype of F[Int]. See examples linked above.

[samuelgruetter]

Do you create a new specialized trait Foo_sp? If so, you could constrain its type parameter:

trait Foo_sp[+A <: Int] {
   ...
}

[DarkDimius]

Do you create a new specialized trait Foo_sp?

This does not matter.

Ok, let me clear this up step-by-step.
Lets say we have:

trait A[+T] {
  def foo[@specialized(Int) B >: T]: A[B] = {
    def id[X](t: X) = t
    id[A[B]](this)
    val s: A[B] = this
    s
  }
}

specialization will duplicate this method, creating:

trait A[+T] {
 // specialization for integers. 
 // you get it by replacing all references to `B` by `Int` in types.
  def foo_sp_Int[B >: T <: Int]: A[Int] = { 
    def id[X](t: X) = t
    id[A[Int]](this) // does not typecheck, this is not a subtype of A[Int]
    val s: A[Int] = this // does not typecheck, this is not a subtype of A[Int]
    s // does not typecheck, this is not a subtype of A[Int]
  }

  // generic version, no changes
  def foo[B >: T]: A[B] = { 
    def id[X](t: X) = t
    id[A[B]](this)
    val s: A[B] = this
    s
  }
}

[samuelgruetter]

I see... So as a Scala user, you would use an ascription to give the compiler a hint: (this: A[B]). You could do the same in specialization (using the Typed AST node), but I guess you want a solution where you don't need to insert anything...

Btw thanks for editing trait A[T] into trait A[+T] ;-)

[DarkDimius]

So as a Scala user, you would use an ascription to give the compiler a hint: (this: A[B])

Type ascription does not work here, as it is typechecked, and typechecking it will fail. Type casts work, but they are spliced everywhere in more-or-less compicated code.

[samuelgruetter]

We have A[T] <: A[B] <: A[Int]. The typechecker can establish both A[T] <: A[B] and A[B] <: A[T], but not A[T] <: A[Int], so you could make it work by ascribing the expression with the middle type A[B], so you reduce the impossible step to two possible ones.

[DarkDimius]

Ok, I get it now. It could indeed work.
The problem is that T could be in more complicated types than A[T], eg Function1[Function1[T, Int], T] and I'm not aware how to synthesize a middle type in a general case.

[adriaanm]

How about dropping the definition of B entirely and putting a constraint in the context for the method body? Can dotty type check modulo constraints (like [HM[X]](Type Inference with Constrained Types - LAMP | EPFL))?

def foo_sp_Int: A[Int] where B =:= Int /\ B >: T

[VladUreche]

@DarkDimius, what you need is the ability to inject the information that T <: Int when type-checking foo_sp_int. Is there any way to do this?

As an alternative, you can do the shallow transformation, like I do in miniboxing, and you wouldn't run into this problem (e.g. List[B] stays List[B], doesn't become List[Int]).