<untyped> error in generated `getType` due to variance annotation

[romac]

The following testcase fails with an <untyped> error somewhere inside the generated assume block in the lambda q => q.cont, which seems related to the type encoding.

import stainless.lang._
import stainless.annotation._

object bug {

  class In[A] {
    @extern @library
    def ?[B](f: A => B): B = {
      ???
    }
  }

  class Out[-A]
  case class Q(cont: Out[BigInt])

  def f(c: In[Q]) = {
    c ? { q => q.cont }
  }
}

Same with a covariant Out.

This error goes away if we leave out the variance annotation on Out. I get the same error on master, #78, and #111.

[samarion]

There's an error at https://github.com/epfl-lara/stainless/blob/9adcdf8ea99766062f511666c0829b4c316bc977/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L840, it should be

let("res" :: obj, ...

The variance annotation only changes Out to a non-ADT and invokes the type encoder.

[romac]

Thanks! The error indeed goes away with that fix :)

The problem is now that thousands of verification conditions are now being generated, and even after letting Stainless run for 5min there were still more to go over.

I tried adding concrete descendants of In and Out (see below) but am now hitting an invalid assertion at https://github.com/epfl-lara/inox/blob/bda6e001a95cd17d6c8166c856474d237426309c/src/main/scala/inox/ast/Paths.scala#L82-L92.

import stainless.lang._
import stainless.annotation._

object InOut {

  sealed abstract class In[+A] {
    @extern
    @library
    def ?[B](f: A => B): B = {
      ???
    }
  }

  case class LocalIn[+A]() extends In[A]

  sealed abstract class Out[-A] {
    def create[B](): (In[B], Out[B])

    def !(msg: A): Unit = {}
  }

  case class LocalOut[-A]() extends Out[A] {
    def create[B](): (In[B], Out[B]) = {
      (LocalIn[B](), LocalOut[B]())
    }
  }

  case class Q(q: Boolean, cont: Out[R])
  case class R(p: BigInt)

  def f(c: In[Q]) = {
    c ? { q => q.cont ! R(42) }
  }

  def g(c: Out[Q]) = {
    val (ri, ro) = c.create[R]()
    c ! Q(true, ro)
    ri ? { r =>
      // do something
    }
  }
}

[samarion]

The assertion failure has been fixed. VC checking is still very slow but that's a whole other issue.