Match type subtyping wrongly instantiates types in patterns

[OlivierBlanvillain]

There is something off with match type subtyping:

trait Inv[T]
object Test {
  def ev[X] = implicitly[
    (X match { case Inv[t] => Int }) =:=
    (X match { case Inv[t] => t })
  ]
}

==> isSubType internal.MatchCase[Inv[t], Int] <:< internal.MatchCase[Inv[t], t] ?
  ==> isSubType Inv[t] <:< Inv[t] ?
  <== isSubType Inv[t] <:< Inv[t]  = true   
  ==> isSubType Inv[t] <:< Inv[t] ?
  <== isSubType Inv[t] <:< Inv[t]  = true   
  ==> isSubType Int <:< t ?                 
    ==> isSubType Int <:< t ?           
      ==> isSubType Int <:< Nothing ?
      <== isSubType Int <:< Nothing  = false  
    <== isSubType Int <:< t  = false        
    ==> lub(Nothing, Int, canConstrain=false)?
    <== lub(Nothing, Int, canConstrain=false) = Int
    ==> isSubType Int <:< Any ?             
    <== isSubType Int <:< Any  = true
  <== isSubType Int <:< t  = true
<== isSubType internal.MatchCase[Inv[t], Int] <:< internal.MatchCase[Inv[t], t] = true

The issue seams to be really match type related, as the following minimization attempt is correctly rejected:

trait M[F[_]]
trait Inv[T]
object Test {
  def ev[X] = implicitly[
    M[[t] =>> internal.MatchCase[Inv[t], t]] =:=
    M[[t] =>> internal.MatchCase[Inv[t], Int]]
  ] // error
}

==> isSubType internal.MatchCase[Inv[t], Int] <:< internal.MatchCase[Inv[t], t] ?
  ==> isSubType internal.type <:< internal.type ?
  <== isSubType internal.type <:< internal.type  = true
  ==> isSubType Inv[t] <:< Inv[t] ?
  <== isSubType Inv[t] <:< Inv[t]  = true
  ==> isSubType Inv[t] <:< Inv[t] ?
  <== isSubType Inv[t] <:< Inv[t]  = true
  ==> isSubType Int <:< t ?
    ==> isSubType Int <:< t ?
      ==> isSubType Int <:< Nothing ?
      <== isSubType Int <:< Nothing  = false
    <== isSubType Int <:< t  = false
  <== isSubType Int <:< t  = false
<== isSubType internal.MatchCase[Inv[t], Int] <:< internal.MatchCase[Inv[t], t] = false