Why is pattern match needed to preserve existential type information?

Question

A blog describing how to use type classes to avoid F-bounded polymorphism (see Returning the "Current" Type in Scala) mentions near its end:

The problem here is that the connection between the types of p._1 and p._2 is lost in this context, so the compiler no longer knows that they line up correctly. The way to fix this, and in general the way to prevent the loss of existentials, is to use a pattern match.

I have verified the code mentioned does not work:

pets.map(p => esquire(p._1)(p._2))

while the other pattern matching variant does:

pets.map { case (a, pa)  => esquire(a)(pa) }

There is also another variant not mentioned which also works:

pets.map{case p => esquire(p._1)(p._2)}

What is the magic here? Why does using case p => instead of p => preserve the existential type information?

I have tested this with Scala 2.12 and 2.13.

Scastie link to play with the code: https://scastie.scala-lang.org/480It2tTS2yNxCi1JmHx8w

The question needs to be modified for Scala 3 (Dotty), as existential types no longer exists there (pun intended). It seems it works even without the case there, as demonstrated by another scastie: https://scastie.scala-lang.org/qDfIgkooQe6VTYOssZLYBg (you can check you still need the case p even with a helper class in Scala 2.12 / 2.13 - you will get a compile error without it).

Modified code with a helper case class:

case class PetStored[A](a: A)(implicit val pet: Pet[A])

val pets = List(PetStored(bob), PetStored(thor))

println(pets.map{case p => esquire(p.a)(p.pet)})

Answer 1

Based on https://stackoverflow.com/a/49712407/5205022, consider the snippet

pets.map { p =>
  val x = p._1
  val y = p._2
  esquire(x)(y)
}

after typechecking -Xprint:typer becomes

Hello.this.pets.map[Any](((p: (A, example.Hello.Pet[A]) forSome { type A }) => {
  val x: Any = p._1;
  val y: example.Hello.Pet[_] = p._2;
  Hello.this.esquire[Any](x)(<y: error>)
}))

whilst the snippet with pattern matching

pets.map { case (a, pa) =>
  val x = a
  val y = pa
  esquire(x)(y)
}

after typechecking becomes

 Hello.this.pets.map[Any](((x0$1: (A, example.Hello.Pet[A]) forSome { type A }) => x0$1 match {
  case (_1: A, _2: example.Hello.Pet[A]): (A, example.Hello.Pet[A])((a @ _), (pa @ _)) => {
    val x: A = a;
    val y: example.Hello.Pet[A] = pa;
    Hello.this.esquire[A](x)(y)
  }
}));

We note that in the latter pattern matching case, the existential type parameter A is re-introduced

val x: A = a;
val y: example.Hello.Pet[A] = pa;

and so relationship between x and y is re-established, whilst in the case without pattern matching the relationship is lost

val x: Any = p._1;
val y: example.Hello.Pet[_] = p._2;