Constructor arguments are not boxed properly during type encoding

[romac]

I'm currently trying to model a typed actor system with Stainless which, as it stands now, requires me to do work with what I would express in plain Scala as a List[Foo[_]] (an existential type).

Here's a simple testcase demonstrating the few ways I tried to express it with Stainless, where methods are annotated with the errors being thrown by Stainless:

object existential {
  case class A()
  case class B()

  sealed abstract class AnyFoo
  case class Foo[T](x: T) extends AnyFoo

  def a: Foo[A] = Foo(A())
  def b: Foo[B] = Foo(B())

  def list0: List[Foo[_]] = List(a, b)
  // Exception in thread "main" stainless.frontend.UnsupportedCodeException: Could not extract type: existential.Foo[_ >: existential.B with existential.A <: Product with Serializable] (class scala.reflect.internal.Types$ExistentialType)

  def list1: List[AnyFoo] = List(a, b)
  // Exception in thread "main" stainless.frontend.UnsupportedCodeException: Could not extract type: existential.Foo[_ >: existential.B with existential.A <: Product with Serializable] (class scala.reflect.internal.Types$ExistentialType)

  def list2: List[AnyFoo] = List(a.asInstanceOf[AnyFoo], b.asInstanceOf[AnyFoo])
  // Insert lenghty inox.ast.TypeOps$TypeErrorException here
}

I get why list0 and list1 cannot be extracted successfully as we currently lack support for existential types, but I had expected list2to succeed.

As another datapoint, here's a testcase which does not involve existential types at all, where methods are again annotated with the errors being thrown:

object no_existential {
  sealed abstract class A
  case class B() extends A
  case class C() extends A

  case class Foo[+T](x: T)

  def b: Foo[B] = Foo(B())
  def c: Foo[C] = Foo(C())

  def list0: List[Foo[A]] = List(b, c)
  // Insert lengthy inox.ast.TypeOps$TypeErrorException here

  def list1: List[Foo[Any]] = List(b, c)
  // Insert lengthy inox.ast.TypeOps$TypeErrorException here

  def list3: List[Foo[A]] = List(b.asInstanceOf[Foo[A]], c.asInstanceOf[Foo[A]])
  // Insert lengthy inox.ast.TypeOps$TypeErrorException here

  def list4: List[Foo[Any]] = List(b.asInstanceOf[Foo[Any]], c.asInstanceOf[Foo[Any]])
  // Insert lengthy inox.ast.TypeOps$TypeErrorException here
}

Is there indeed a problem with the type system that makes the second testcase not type-check successfully or is that that scenerio just unsupported at the moment?

[romac]

I only realised now that the firs testcase above only relies on wildcards, not full-blown existentials (ie. existential types which pass this condition).

While adding support for wildcards doesn't seem out of my reach, they won't actually prove very useful for my use-case, where I actually need something akin to:

trait Wrap {
  type Inner
  def foo: Inner
  def bar(toto: Inner): Wrap
}

def other(a: Int): Wrap = new Wrap { /* ... */ }

val wrapped = new Wrap {
  type Inner = Int
  def foo = 42
  def bar(toto: Int): Wrap = other(toto + bar)
}

I am thus wondering whether I should resuscitate my anonymous classes branch, and then look into associated types/type aliases. What do you think?

[jad-hamza]

Do we need wildcards or existentials to typecheck this testcase (variant of your first testcase)

object existential {
  case class A()
  case class B()

  sealed abstract class AnyFoo
  case class Foo[T](x: T) extends AnyFoo

  val a: AnyFoo = Foo(A())
  val b: AnyFoo = Foo(B())

  val list0: List[AnyFoo] = List(a, b)
}

I wonder if the modifications made by @OlivierBlanvillain in the branch https://github.com/OlivierBlanvillain/stainless/tree/cats are enough

[romac]

No, we don't them for such a variant. But it too fails with a type error as well on master. It also fails to verify on Olivier's branch (I don't have the output on hand right now but I'll post it later). And as far as I can tell, none of the changes in that branch should affect whether such code can be extracted or not.

[jad-hamza]

This fails as well:

object Existential {
  case class A()

  sealed abstract class AnyFoo
  case class Foo[T](x: T) extends AnyFoo

  val a: AnyFoo = Foo(A())
}

[jad-hamza]

I looked at the encoding, and I see that Foo has type: (Type, Object) => Object. Then the issue happens when Foo is called: Foo(Adt(1072, Nil()), A()) is of type untyped Apparently, the type of A() is not a subtype of Object (the inox function isSubtypeOf from TypeOps returns false).

@samarion Should isSubtypeOf return true in that case?

[samarion]

Hi, sorry for not helping much with the debugging, I haven't had time to actually run the examples and see what's going on.

@jad-hamza: in your example, isSubtypeOf is doing the right thing. The class A is specialized to an ADT because it fits into the fragment we know how to convert to ADTs. It therefore lives in a separate domain as the Object hierarchy.

This is an issue with specialized type boxing. It seems that boxing is not being performed for ClassConstructor arguments. To fix this, you can change the argument computation at https://github.com/epfl-lara/stainless/blob/31960ce3e68b0fd8d44480a9470771ece5c38595/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L819-L821 to something resembling https://github.com/epfl-lara/stainless/blob/31960ce3e68b0fd8d44480a9470771ece5c38595/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L848-L850

This should hopefully fix the issue in your example. I'm not sure about the initial issue, I'll need to take a closer look once I have some time.

[romac]

Thank you both for taking the time to look into it! I will take a stab at this, following @samariion’s instructions, and report back.

On 5 Oct 2017, at 13:16, Nicolas Voirol notifications@github.com wrote:

Hi, sorry for not helping much with the debugging, I haven't had time to actually run the examples and see what's going on.

@jad-hamza: in your example, isSubtypeOf is doing the right thing. The class A is specialized to an ADT because it fits into the fragment we know how to convert to ADTs. It therefore lives in a separate domain as the Object hierarchy.

This is an issue with specialized type boxing. It seems that boxing is not being performed for ClassConstructor arguments. To fix this, you can change the argument computation at https://github.com/epfl-lara/stainless/blob/31960ce3e68b0fd8d44480a9470771ece5c38595/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L819-L821 to something resembling https://github.com/epfl-lara/stainless/blob/31960ce3e68b0fd8d44480a9470771ece5c38595/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L848-L850

This should hopefully fix the issue in your example. I'm not sure about the initial issue, I'll need to take a closer look once I have some time.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[samarion]

Fixed by https://github.com/epfl-lara/stainless/pull/78