Вывод подчеркивающих типов

Question

[Мне не удалось объяснить проблему с меньшим количеством слов.Суть проблемы в том, что компилятор выводит тип подчеркивания (_).В частности, [_ >: SomeType <: SomeOtherType].Я понятия не имею, когда, как и почему это возможно]

В качестве упражнения для скалы я пытаюсь закодировать вектор элементов с заданным размером.
В качестве необходимого шага яначалось с копирования существующей кодировки натуральных чисел:

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)
}

Я считаю, что следующая диаграмма является точным изображением отношения типа:
Затем я попытался смоделироватьвектор, параметризованный по типу элементов и другой тип по размеру.Чтобы объяснить проблему, я предположил вектор целых и параметризовал только размер вектора:

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 - я знаю, что возврат that для реализации метода plus в VectorCons не достигает того, что подразумевает семантика 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)

Спасибо за ваш вклад,