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 https://github.com/lampepfl/dotty/issues/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 https://github.com/lampepfl/dotty/issues/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]).

[liufengyun]

@AleksanderBG It seems to me this is related to GADT narrowing. Is there a way to generalize and possibly support this use case?

[abgruszecki]

@liufengyun looking at the comments on the issue, maybe. The fundamental problem I'm seeing is that we only allow adding GADT constraints to type parameters of functions, and all examples in the issue would want to add them to either type members or type parameters of classes, either of which I'd say is non-trivial to soundly allow.