Type of pattern binder variable on RHS does not correspond to matched pattern on LHS

Why does the partial function

val warpedEngineers: PartialFunction[Warped[Crewmember], Warped[Engineer]] = {
  case v@Warped(Engineer(name: String)) => v.asInstanceOf[Warped[Engineer]]
}

seem to require asInstanceOf cast on RHS whilst the following does not

val engineers: PartialFunction[Crewmember, Engineer] = {
  case v@Engineer(name) => v
}

given

sealed trait Crewmember
case class Engineer(name: String) extends Crewmember
case class Commander(name: String) extends Crewmember

case class Warped[+A <: Crewmember](v: A)

val engineers: PartialFunction[Crewmember, Engineer] = {
  case v@Engineer(name) => v
}

val warpedEngineers: PartialFunction[Warped[Crewmember], Warped[Engineer]] = {
  case v@Warped(Engineer(name: String)) => v.asInstanceOf[Warped[Engineer]]
}

val crew: List[Crewmember] = 
  List(Engineer("Geordi"), Commander("Picard"), Engineer("Scott"), Commander("Kirk"))

val warpedCrew: List[Warped[Crewmember]] = 
  List(Warped(Engineer("Geordi")), Warped(Commander("Picard")), Warped(Engineer("Scott")), Warped(Commander("Kirk")))

crew collect engineers
// res0: List[Engineer] = List(Engineer(Geordi), Engineer(Scott))

warpedCrew collect warpedEngineers
// res1: List[Warped[Engineer]] = List(Warped(Engineer(Geordi)), Warped(Engineer(Scott)))

Casting with asInstanceOf could be avoided like so

case Warped(eng: Engineer) => Warped(eng) 

but I am wondering why does compiler not insert implicit asInstanceOf and instead types v to Warped[Crewmember]

val warpedEngineers: PartialFunction[Warped[Crewmember], Warped[Engineer]] = {
  case v@Warped(Engineer(name: String)) => v 
}

Error: type mismatch;
 found   : Warped[Crewmember]
 required: Warped[Engineer]
      case v@Warped(Engineer(name: String)) => v

According to SLS 8.1.3: Pattern Binders

A pattern binder 𝑥@𝑝 consists of a pattern variable 𝑥 and a pattern 𝑝. The type of the variable 𝑥 is the static type 𝑇 implied by the pattern 𝑝. This pattern matches any value 𝑣 matched by the pattern 𝑝, and it binds the variable name to that value.

A pattern 𝑝 implies a type 𝑇 if the pattern matches only values of the type 𝑇.

Warped(Engineer(name)) on the left in

case v@Warped(Engineer(name: String)) => v

has static type Warped[Crewmember] because that's what you wrote in the type signature

val warpedEngineers: PartialFunction[Warped[Crewmember], ...

So if you write just v on the right it's a type mismatch.

Warped(Engineer(name)) on the right and on the left in

case Warped(Engineer(name)) => Warped(Engineer(name))

look similar but are different because they have different types. They are actually Warped[Crewmember](Engineer(name)) and Warped[Engineer](Engineer(name)). Because of covariance Warped[Engineer] is a Warped[Crewmember] but not vice versa.

How is compiler supposed to guess that it should insert asInstanceOf here and shouldn't for example in val x: Int = "a"?

If you change the signature

val warpedEngineers: PartialFunction[Warped[Engineer], Warped[Engineer]] = {
  case v@Warped(Engineer(name)) => v
}

then static type of v will be Warped[Engineer] and the code will compile.

Similarly if you use typed pattern

val warpedEngineers: PartialFunction[Warped[Crewmember], Warped[Engineer]] = {
  case v: Warped[Engineer] => v
}

then static type of v will be Warped[Engineer] and the code will compile.

It seems in terms of specification pattern v@Warped(Engineer(name)) in

val warpedEngineers: PartialFunction[Warped[Crewmember], Warped[Engineer]] = {
  case v@Warped(Engineer(name)) => ...
}

"implies" type Warped[Crewmember] (because of the signature).