Dotty: Recursive extension method using implicit argument with generic fails to infer correct types

[micheal-hill]

Minimized code

enum AList[+A] {
  case Cons(head: A, tail: AList[A])
  case Nil
}

object AList {
  extension [A](l: AList[A]) def sum(using numeric: Numeric[A]): A = l match {
    case Cons(x, xs) => numeric.plus(x, xs.sum(using numeric))
    case Nil         => numeric.zero
  }
}

Output

Compiler error at line 10:

Found:    (numeric : Numeric[A])
Required: Numeric[A$1]

where:    A   is a type in method extension_sum with bounds >: A$1
          A$1 is a type in method extension_sum with bounds <: A

Dropping the explicit parameter list when calling sum recursively results in the error:

value sum is not a member of AList[A$1].
An extension method was tried, but could not be fully constructed:

    AList.extension_sum[A$1](xs)(numeric)

where:    A$1 is a type in method extension_sum with bounds <: A

Scastie repro to demonstrate both.

Expectation

Expect that this should compile and allow (explicitly or not) the given numeric instance to be used for the recursive call.
From chat with @smarter here:

yeah type inference is being too eager and instantiating the type parameter of sum before typing the second argument
so it ends up choosing the pattern-bound A$1 instead of A

[smarter]

It's worth noting that it works if the type parameter is passed explicitly (xs.sum[A]) or sum is rewritten as a non-extension method

[smarter]

Ha, I've just now realized why this gives the compiler trouble in the first place, the issue is that:

case Cons(head: A, tail: AList[A]) extends AList[A]

is translated to a case class Cons with an invariant type parameter A, if instead we explicitly make it covariant:

case Cons[+A](head: A, tail: AList[A]) extends AList[A]

then the job of type inference becomes much easier. We should probably tweak the extension method desugaring to keep the declared variance in the enum type.

[bishabosha]

@smarter is there any reason to not copy the variance to the Cons case in desugaring?

[smarter]

I don't think so

[bishabosha]

linking #9260 as related

[LPTK]

@bishabosha

@smarter is there any reason to not copy the variance to the Cons case in desugaring?

Because you may have cases whose variance does not agree?

enum AList[+A] {
  case Cons(head: A, tail: AList[A])
  case Nil
  case Foo(head: A => A) // legal and valid
}

[smarter]

Ah yeah, so we'd need to check if the variance is fine first.

[LPTK]

Wouldn't it be better to fix type inference instead of adding more special cases to the already-nontrivial enum desugaring? Why does type inference fail here?

[smarter]

Fixing type inference is always a good idea sure :). But I think that's less important than figuring out what to do with enums, in particular I think it's legitimate for people to expect variance to be propagated to the enum cases, and the fact that it isn't can lead to confusing errors (even with perfect type inference).

[LPTK]

The way I see it, there are two possibilities:

• enum desugars consistently, without surprises, and if you want variant cases you go the long way for expressing it: case Cons[+A](head: A, tail: AList[A]) extends AList[A]

• enum desugars differently depending on very subtle conditions, leading to some definitions type-inferring better in some situations and some not, without a good way of understanding why, making the whole thing seem magical. Example related situations where this would be a problem:

  • I made some previously-covariant class invariant, and this has silently made my enum's case invariant (because it had a field of this type), introducing type inference and type checking problems in seemingly-unrelated code;

  • I wrote a class Foo[A] forgetting to make it covariant, and used it in an enum case, blocking the enum's covariance, but the compiler is not telling me that, instead yielding strange errors in unrelated places.

the fact that it isn't can lead to confusing errors (even with perfect type inference).

What sort of errors are you thinking about? (Besides e.g., having Cons[Int] <: Cons[Any] fail, as expected).

[smarter]

Yeah it's not clear-cut that it's a good idea, I think either way can be confusing.

What sort of errors are you thinking about?

For starter, the sort of things we're seeing in this issue, where xs has type Cons[A$1] where A$1 <: A because it's invariant, which complicates everything (even though in this particular case we should have enough information through the expected type to do the right thing)

[smarter]

Another possibility would be to always desugar while preserving the variance, and force the user to write [A] explicitly in situation where that doesn't variance-check. That way the desugaring stays simple and it's very easy to see where you have an invariant case (which among other things complicates pattern-matching as mentioned above, so it's good to be aware of it)

[LPTK]

For starter, the sort of things we're seeing in this issue, where xs has type Cons[A$1] where A$1 <: A because it's invariant, which complicates everything

I'm still not sure why this causes trouble in the type inference. When it sees xs.sum, it should introduce a type variable ?X which is known to be a supertype of A$1, and then it should unify ?X with A seeing that we're passing using numeric, of type Numeric[A]. Is it that whenever there is an implicit argument section it automatically bails and instantiates everything, even though no implicit search actually occurs?

[smarter]

Is it that whenever there is an implicit argument section it automatically bails and instantiates everything, even though no implicit search actually occurs?

Something like that yes, and of course we should fix that, but there's situations where you don't have an explicit using argument and you don't have an expected type (e.g. in val z = xs.sum, the inferred type variable for sum is ?A >: A$1 where A$1 <: A, the compiler instantaties ?A := A$1 and then does an implicit search for Numeric[A$1] which doesn't find anything because Numeric is itself invariant, it would work if the compiler didn't instantiate ?A before doing the search, but we'd need a good heuristic for doing that since in general that can lead to ambiguous implicits.