Implicit resolution with type bound for intersection type fails

[pweisenburger]

The following code compiles using Scala:

object test { 
    trait A 
    trait B 
    trait Wrapper[T] 
   
    trait Relation[T, U] 
    implicit def relation[T <: Wrapper[U], U]: Relation[T, U] = ??? 
   
    def test(implicit ev: Relation[Wrapper[A] with Wrapper[B], B]) = ??? 
    test 
  }

Dotty produces the following compiler error:

10 |    test
   |        ^
   |no implicit argument of type test.Relation[test.Wrapper[test.A] & test.Wrapper[test.B], test.B] was found for parameter ev of method test in object test.
   |I found:
   |
   |    test.relation[Nothing, Nothing]
   |
   |But method relation in object test does not match type test.Relation[test.Wrapper[test.A] & test.Wrapper[test.B], test.B].

Notably, using

def test(implicit ev: Relation[Wrapper[A] with Wrapper[B], A]) = ??? 

instead of

def test(implicit ev: Relation[Wrapper[A] with Wrapper[B], B]) = ??? 

works fine (i.e., the implicit value is successfully resolved).

[smarter]

Since Wrapper is invariant in its type argument T, can you even construct a value whose type is a subtype of Wrapper[A] with Wrapper[B] ?

[pweisenburger]

I think you're right, you cannot actually construct a value of type Wrapper[A] with Wrapper[B]. In my case, a value of such a type is never constructed. The type is basically some kind of phantom and only appears as type parameter carrying some further information to get a bit of additional type-safety.

[Blaisorblade]

Notably, [...]

I suspect that's due to the incompleteness of the constraint solver; a complete solution would require backtracking, which could make typechecking exponentially slower.
Implicit search must instantiate relation[?T, ?U]: Relation[?T, ?U] so that

Relation[?T, ?U] <: Relation[Wrapper[A] & Wrapper[B], B]
?T <: Wrapper[?U]
// hence
?T = Wrapper[A] & Wrapper[B] <: Wrapper[?U]
?U = B

but at some point, Wrapper[A] & Wrapper[B] <: Wrapper[?U] only checks Wrapper[A] <: Wrapper[?U] and doesn't backtrack to Wrapper[B] <: Wrapper[?U], which you'd need.

That's internally documented in

https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L643-L658
https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L960-L989

[pweisenburger]

Okay, thanks for the explanation. That makes sense indeed. And I see the point in avoiding the need for backtracking during typechecking.

But from a programming perspective, it's a bit strange that it makes a difference whether you write A & B or B & A. I don't know if it could make sense to backtrack in certain situations like this. Also not sure how common the occurrence of intersection types is in real code and if this would even decrease typechecking speed significantly in practice.

Otherwise, it might be good to at least augment the "no implicit argument found" warning with a hint that a branch of the search space was cut off due to an intersection type B & A. It's hard to debug otherwise since the behavior is not really intuitive.

[smarter]

I don't know if this is ok for your usecase, but note that your example can be made to compile by making Wrapper covariant in T (trait Wrapper[+T])

[pweisenburger]

Good point, thanks! In the simplified example here this is a solution. But unfortunately, in my specific use case, I cannot easily make T covariant (the intersecting types could also be different, e.g., WrapperA[T] with WrapperB[U]).

[Blaisorblade]

TLDR: constraints in this example can be reordered to help Dotty, I wonder if Dotty's heuristics could be improved to handle this case by instantiating ?U first, and I agree that logging cuts during constraint solving could be useful (also for #4029).

But from a programming perspective, it's a bit strange that it makes a difference whether you write A & B or B & A.

I totally agree — but at long as nobody implements and benchmarks backtracking and shows it's fine, we risk this sort of trouble.

In this case backtracking might not be necessary tho. I must say: I expect instantiating ?U first would help dotty see that indeed Wrapper[A] & Wrapper[B] <: Wrapper[B]. I suspect the only problematic backtracking is when you need to instantiate type variables but later retract those instantiations.
Maybe Dotty can be fixed to do it, but it seems to me the instantiation heuristics are pretty subtle. @smarter

Meanwhile, maybe one could also tune the method signature somehow to help inference — here, one could try something like:

implicit def relation[T, U](/* erased? */ implicit ev: T <:< Wrapper[U]): Relation[T, U] = ??? 

which apparently just works (surprising, since it was the first attempt)!

object test { 
    trait A 
    trait B 
    trait Wrapper[T] 
   
    trait Relation[T, U] 
    implicit def relation[T, U](/* erased? */ implicit ev: T <:< Wrapper[U]): Relation[T, U] = ??? 
   
    def test(implicit ev: Relation[Wrapper[A] with Wrapper[B], B]) = ??? 
    test 
  }

Otherwise, it might be good to at least augment the "no implicit argument found" warning with a hint that a branch of the search space was cut off due to an intersection type B & A

I agree such warnings might be very useful, and we have other reasons why being able to detect incomplete search might be useful (#4029).

It'd also be useful to have a debugger for type inference (à la https://infoscience.epfl.ch/record/179877/files/typedebugger-applc2012.pdf), but the amount of effort required for last attempt was very significant.

[pweisenburger]

I totally agree — but at long as nobody implements and benchmarks backtracking and shows it's fine, we risk this sort of trouble.

That would of course be the best solution. But I understand that you don't want to risk the slowdown as long as there is no evidence that this kind of backtracking does not come at a significant performance cost. Issuing a more meaningful warning is maybe a more practical solution. Since it seems it would be good to detect an incomplete search anyway.

In this case backtracking might not be necessary tho. I must say: I expect instantiating ?U first would help dotty see that indeed Wrapper[A] & Wrapper[B] <: Wrapper[B].

Interesting; that might already catch quite some problematic cases without backtracking.

Meanwhile, maybe one could also tune the method signature somehow to help inference — here, one could try something like:

implicit def relation[T, U](/* erased? */ implicit ev: T <:< Wrapper[U]): Relation[T, U] = ???

which apparently just works (surprising, since it was the first attempt)!

Thanks! That seems to help type inference for my case indeed.

[odersky]

Closing since this has been inactive for a long time, and there are no clear directives what should be done.

[Blaisorblade]

Since you forgot to close.