Problems with generic abstract types

Question

I have an abstract Stack type as follows

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

I would like to verify that pop returns the last pushed element:

// 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

The two lemmas are equivalent, but Leon fails to identify the type parameters in the second lemma. Interestingly, Leon has no problem when Stack is concrete or non-generic (see the link below for examples). Is this a feature of Leon or just a bug?

The full example code can be found here.

Answer 1

I tried the example in your gist link (under "can be found here") and it works in the current version of Leon, both online and in the git repository. So, if this was a bug, it is fixed now. If you have any related questions, we are happy to answer, because Leon supports only objects and case classes at this time, so there are differences compared to full Scala.