下划线类型的推断

Question

[我无法用较少的冗长来解释问题.问题的核心是编译器推断出一个下划线(_)类型.特别是[_ >: SomeType <: SomeOtherType].关于何时,如何以及为何可能,我一无所知

作为一个scala练习,我试图编码给定大小的元素向量.
作为必要的步骤,我开始复制现有的自然数编码:

sealed trait Natural extends Product with Serializable {
  def +(that: Natural): Natural
}

case object Zero extends Natural {
  override def +(that: Natural): Natural = that
}

final case class Suc[N <: Natural](n: N) extends Natural {
  override def +(that: Natural): Natural = Suc(n + that)
}

我相信下面的图表是对类型关系的忠实描绘:
然后,我试图模拟由元素上的类型和大小上的另一个类型参数化的向量.为了解释这个问题,我假设了一个int的向量,并且只参数化了向量的大小:

import shapeless.=:!=  

sealed trait Vector[+Size <: Natural] extends Product with Serializable {
  def head: Int
  def tail: Vector[Natural]

  def plus[OtherSize >: Size <: Natural]
  (that: Vector[OtherSize])
  (implicit ev: OtherSize =:!= Natural): Vector[OtherSize]
}

case object VectorNil extends Vector[Zero.type] {
  override def head: Nothing = throw new Exception("Boom!")
  override def tail: Vector[Zero.type] = throw new Exception("Boom")

  override def plus[OtherSize >: Zero.type <: Natural]
  (that: Vector[OtherSize])
    (implicit ev: =:!=[OtherSize, Natural]): Vector[OtherSize] = this

}

final case class VectorCons[N <: Natural](
  head: Int,
  tail: Vector[N]
) extends Vector[Suc[N]] {

  override def plus[OtherSize >: Suc[N] <: Natural]
  (that: Vector[OtherSize])
    (implicit ev: =:!=[OtherSize, Natural]): Vector[OtherSize] = that
}

请注意,这VectorCons[N]实际上是一个大小的矢量Suc[N].(延伸Vector[Suc[N]]).
方法plus应该添加两个相同大小的向量的元素.我想提升到类型级别的验证,你只能对相同大小的向量求和.
请注意,类型边界OtherSize >: Size <: Natural与隐式证据的结合应该实现(参见底部的类似示例),但是:

val foo = VectorCons(1, VectorCons(2, VectorNil))
//type -> VectorCons[Suc[Zero.type]]
// note that foo is (can be viewed) as Vector[Suc[Suc[Zero.type]], i.e
// a vector of 2 elements

val bar = VectorCons(3, VectorNil)
//type -> VectorCons[Zero.type]

val baz = foo.plus(bar)
//type -> Vector[Suc[_ >: Suc[Zero.type] with Zero.type <: Natural]]  !! How is this possible ?? !!

对我的沮丧,baz编译得很好!! 无形的约束不起作用; 好吧,因为OtherSize真的不同于Natural; 特别是,它是Suc[_ >: Suc[Zero.type] with Zero.type <: Natural].
所以,我对这种类型非常困惑baz!这是允许绕过约束的原因.

1. 编译器推断出baz/ 的类型是bar什么？
2. 这是一种存在主义类型吗？
3. 是否允许编译器推断出这样的事情？
4. 这不是不受欢迎的行为吗？

此时,我不关心这是否是向量的正确编码.只是想了解编译器如何推断出该类型baz？

ps
1 - 我知道VectorCons上that方法实现的返回plus并没有实现plus语义所暗示的,但这对于这个问题并不重要.

###### Extra #######
我怀疑这种奇怪的行为(至少对我而言)行为与自然数字有关.以下代码工作正常!! :
[忽略代码的荒谬语义]

  sealed trait Animal extends Product with Serializable
  case class Dog() extends Animal
  case class Cow() extends Animal
  case object NoBox extends Animal //Not important

和,

trait Vector[+A <: Animal] {
  def head: A

  def plus[That >: A <: Animal]
  (that: Vector[That])
    (implicit ev: =:!=[That, Animal]): Vector[That]
}

case object Nil extends Vector[NoBox.type] {
  def head: Nothing = throw new NoSuchElementException("Boom!")

  override def plus[That >: NoBox.type <: Animal]
  (that: Vector[That])(implicit ev: =:!=[That, Animal]): Vector[That] = this
}

case class Cons[A <: Animal](head: A) extends Vector[A] {

  override def plus[That >: A <: Animal]
  (that: Vector[That])(implicit ev: =:!=[That, Animal]): Vector[That] = that
}

其中:

val foo = Cons(Dog())
val bar = Cons(Cow())

// Compiles
val baz = foo.plus(foo)
val baz2 = bar.plus(bar)

// Does not compile  (what I would expect)  
val baz3 = bar.plus(foo)
val baz4 = foo.plus(bar)

谢谢您的意见,