Constructor arguments are not boxed properly during type encoding

[epfl-lara]

Constructor arguments are not boxed properly during type encoding

[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

stainless/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala

Lines 819 to 821 in 31960ce

	case s.ClassConstructor(ct, args) =>
	val fd = classConstructors(ct.id)
	t.FunctionInvocation(fd.id, Seq(), ct.tps.map(encodeType) ++ args.map(transform))

to something resembling

stainless/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala

Lines 848 to 850 in 31960ce

	val newArgs = (fd.params zip args).map { case (vd, arg) =>
	unifyTypes(transform(arg), transform(arg.getType), fdScope.transform(vd.tpe))
	} ++ tps.map(encodeType)

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 ***@***.***> 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 #78