Implicit resolution does not take type path into account

[LPTK]

Compiler version

3.0.2

Minimized code

It's often useful to architect modules with some shared parts, as in:

trait Shared:
  class E

object ImplA extends Shared { /* ... */ }
object ImplB extends Shared { /* ... */ }

But we are kind of stuck when we want to provide type class instances that work on all shared parts. I think this approach ought to work, but currently does not:

trait Shared:
  class E

given ImplA: Shared with { /* ... */ }
given ImplB: Shared with { /* ... */ }

// The type class of interest:
class Bar[A]
object Bar:
  given (using s: Shared): Bar[s.E] = ???

Output

summon[Bar[ImplA.E]]

ambiguous implicit arguments of type Playground.Bar[Playground.ImplA.E] found for parameter x of method summon in object Predef.
I found:

    Playground.Bar.given_Bar_E(
      /* ambiguous: both object ImplA in object Playground and object ImplB in object Playground match type Playground.Shared */
        summon[Playground.Shared]
    )

But both object ImplA in object Playground and object ImplB in object Playground match type Playground.Shared.

summon[Bar[ImplA.E]](using Bar.given_Bar_E)

ambiguous implicit arguments: both object ImplA in object Playground and object ImplB in object Playground match type Playground.Shared of parameter s of given instance given_Bar_E in object Bar

summon[Bar[ImplA.E]](using Bar.given_Bar_E(using ImplA))

Ok.

Expectation

Implicit resolution should work out that the choice of ImplA or ImplB is not actually ambiguous.

[odersky]

I agree this would be desirable, but it's starting to look like global type inference. So yes, if someone figures it out how to do that without compromising other aspects including compiler speed, I'd be happy to review and merge.

[LPTK]

The funny thing is that this sort of inference already works well based on the type arguments of types being looked up by implicit resolution.

For example, there are easy (but awkward and ugly) workarounds that expose the right instance to choose to the compiler via a type argument, as in:

trait Tagged[X]

trait Shared[A]:
  class E extends Tagged[A]

given ImplA: Shared[ImplA.type] with {}
given ImplB: Shared[ImplB.type] with {}

class Bar[A]
object Bar:
  given [A](using s: Shared[A]): Bar[s.E & Tagged[A]] = ???

summon[Bar[ImplA.E]] // Ok!

I just don't really understand why implicit resolution does this reasoning based on type arguments but stops short of including the prefix of types in the inference reasoning as well.

In other words: in the workaround code, Dotty realizes that to unify s.E & Tagged[A] with ImplA.E, it can't pick s = ImplB as that would mean A = ImplB.type, yielding an incompatible Tagged[ImplB.type] instead of Tagged[ImplA.type], so it rules out this case. In the original code, why can't we reason that we can't pick s = ImplB because that would result in an incompatible prefix ImplB for the type s.E?

[odersky]

I just don't really understand why implicit resolution does this reasoning based on type arguments but stops short of including the prefix of types in the inference reasoning as well.

It's probably because to reason what E is it wants s to be resolved first. It's a complicated area. There's the source code to play with to find out more.