scala - ジェネリック抽象型の問題

Question

次のような抽象的なスタック型があります

abstract class Stack[T] {
  def empty  : Stack[T]
  def pop () : (Option[T], Stack[T])
  def push (e : T) : Stack[T]
  def size : BigInt
}

pop最後にプッシュされた要素を返すことを確認したいと思います:

// ok
def test_v1[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 match {
    case Some(e2) => e == e2
    case _        => false
  }
} holds

// failed
def test_v2[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 == Some(e)
} holds

2 つの補題は同等ですが、Leon は 2 番目の補題の型パラメーターを識別できません。興味深いことに、Leon は Stackが具体的であっても非ジェネリックであっても問題ありません (例については、以下のリンクを参照してください)。これは Leon の機能ですか、それとも単なるバグですか?

完全なサンプル コードはここにあります。