Incorrect given resolution with abstract type parameter and same type constructor

[heaven-born]

Compiler version

3.0.0-RC2

Minimized code

    trait Test[T]

    given [K]: Test[List[String] & K] with {}

     summon[Test[List[String] & Int]] // compiles
     summon[Test[List[String] & List[Int]]] // doesn't 
     summon[Test[List[String] & Option[Int]]] // compiles again

Output

no implicit argument of type  Test[List[String] & List[Int]] ...

Expectation

Not sure how it works with HKT, but I expected all of them to compile.

[odersky]

List[String] & List[Int] gets simplified to List[String & Int] and then it does not match the intersection anymore.

Generally, matching on intersection is a bad idea since they are not rigid enough.

[heaven-born]

it this simplification apply to invariant type parameters as well?
Because this doesn't work either:

    trait Has0[T]
    trait Test[T]

    given [K]: Test[Has0[String] & K] with {}

    summon[Test[Has0[String] & Has0[Int]]]

@odersky

[odersky]

A good way to find out more about these things is to pass the given that you think should match to the summon.
Then you see:

-- [E007] Type Mismatch Error: ../new/test.scala:6:57 --------------------------
6 |    val x = summon[Test[Has0[String] & Has0[Int]]](using g[)
  |                                                         ^
  |                                  Found:    g[Nothing]
  |                                  Required: Test[Has0[String] & Has0[Int]]

longer explanation available when compiling with `-explain`

The compiler inferred g to have type parameter Nothing. If we pass the expected type, it works:

summon[Test[Has0[String] & Has0[Int]]](using g[Hash0[Int]])  // ok

So yes, in the presence of intersection types you will not get very good type inference.

[heaven-born]

is it possible to fix it in the compiler? I see a lot of ways how this kind of type inference can be used in ZIO for type-level programming. ZIO has its "HAS pattern" and it would be useful to have implicit resolution works this way for replacing one Has to another Has on compile time.
@odersky