givens synthesis question

[NPCRUS]

hello folks, i don't really know right words to describe this behavior, but i will try my best, having such code(https://scastie.scala-lang.org/bcGe9yspStSHqXfdsplVMQ):

trait EqProxy[A, B]

object EqProxy {
  given [A, B](using A =:= B): EqProxy[Option[A], B] = new EqProxy {}
}

summon[EqProxy[Option[String], String]]
summon[EqProxy[Option[String], Int]]

first summon compiles, second one doesn't(i expected both to not compile)
the way i see it, is that the first type param of return type of given Option[A] somehow removes Option from type parameter A so that =:= summons equality between String =:= String and not Option[String] =:= String. this is the best way i can describe it.

Are there any docs on this behavior, or maybe there's a better well explained underlying mechanism that does this and not what I imagine? Thanks in advance

[som-snytt]

-Vprint:typer or -Vprint:inlining tells you what it did.

        {
          val x$proxy1: EqProxy[Option[String], String] =
            EqProxy.given_EqProxy_Option_B[String, String](<:<.refl[String])
          x$proxy1
        }

So A and B are both String.

Your result happens to implicate Option[A], and you expect a result in Option[String], so that aligns.

Edit: I see maybe you think your type args to summon are the args to your given def, so -Vprint clears that up.