Scala type inference breaking down in obvious setting?

Question

I have a rather simple piece of code that does not compile, as a type can apparently not be inferred. I would like to understand why it does not, as I have plenty of type annotations, and it should work. The code is

object MyApp {

  trait A { 
    type V
    val value: V
  }

  case class ConcreteA(value: Int) extends A { type V=Int }

  def convert[T<:A](v: T#V): T = ConcreteA(v.asInstanceOf[Int]).asInstanceOf[T] // brief method with casts for illustration purposes only


  def main(args: Array[String]) {
    val i: Int = 10
    val converted: ConcreteA = convert(i)
  }

}

(It compiles if I add an explicit [ConcreteA] on the convert-call)

The error I get is

MyApp.scala:19: error: no type parameters for method convert: (v: T#V)T exist so that it can be applied to arguments (Int)
 --- because ---
argument expression's type is not compatible with formal parameter type;
 found   : Int
 required: ?T#V
    val converted: ConcreteA = convert(i)
                               ^
MyApp.scala:19: error: type mismatch;
 found   : Int
 required: T#V
    val converted: ConcreteA = convert(i)
                                       ^
MyApp.scala:19: error: type mismatch;
 found   : T
 required: MyApp.ConcreteA
    val converted: ConcreteA = convert(i)
                                      ^
three errors found

Can anyone explain this to me?

Edit: I expected Scala to deduce that T is ConcreteA here. I did so because the result of the convert call goes into a val type annotated as such.

Answer 1

The problem, as far as I know, is that type inference works using the Unification algorithm, which simply will try to satisfy the constraints for the given values. It will first try to prove that the input v satisfy the type T#V, but at this moment, it does not have any information about T thus it simply fails before checking if the result type satisfy the condition.
If you explicitly specify that T is ConcreteA then it will be able to continue.

However, you can make it work by postponing the type checking of the arguments after the inference, using Generalized Type Constraints.

def convert[T <: A, V](v: V)(implicit ev: V <:< T#V): T = ???

val converted: ConcreteA = convert(10)
// converted: ConcreteA = ConcreteA(10)

val converted: ConcreteA = convert("hey")
// Compile error:  Cannot prove that String <:< T#V.

In this case the value v does not have any restrictions, thus the compiler simple bind V to the type of v which it already knows what it is. Then, it checks the return type T which it knows must be a ConcreteA, which satisfy the constraint that it must be a subtype of A, thus it pass.
After having solved the inference, the compiler attempts to solve the implicits. In this case, it needs to obtain (prove) that V <:< T#V, which in the first case works, but in the second fails.