Inconsistent normalization of parametrized types using (externes) type aliases

[saraswat]

The code (extracted, after a few hours of loving labor, from a real program):

import stainless.annotation.extern
object CheckArray {
  @extern type MyInt = Int
  @extern type AA = Array[MyInt]
  case class A(x:Array[MyInt])
  def m(x: Array[MyInt]): MyInt = A(x).x(0)
}

yields

error] /Users/savija/IdeaProjects/cake/stainless_test/verified/src/main/scala/CheckArray.scala:8:16: Type error: this.x, expected Array[Int], 
[error] found Array[MyInt]
[error] 
[error] Typing explanation:
[error] this.x is of type Array[MyInt]
[error]   this is of type A
[error]   case class A(x:Array[MyInt] /* AA*/)
[error]                ^
[error] The extracted sub-program is not well formed.

I would hope that the same code is called to normalize the type in both places, and should yield Array[Int] in both places.

The workaround for now is:

mport stainless.annotation.extern
object CheckArray {
  @extern type MyInt = Int
  @extern type AA = Array[MyInt]
  case class A(x:AA])
  def m(x: AA): MyInt = A(x).x(0)
}

It would be helpful to understand exactly how @extern type A = <typeexpr> is supposed to operate. What exactly is an opaque type (as implemented in Stainless). How is equality of types expressions specified, if sub-expressions are opaque types.

To be clear, the original problem I had (which will take some time to reproduce with a small example) resulted in a traceback because types did not match, the type Array[OrderT] did not match the type Array[?]. The first type comes from the definition (case class Foo(x: Array[OrderT]...), the second came from an invocation within a method m, using an arg that was a parameter of m, whose type was also declared as Array[OrderT]. This took a lot of head-scratching to figure out...

[vkuncak]

Does issue come up with types other than arrays (e.g. Lists of external types)?

[saraswat]

Interesting. Works for Option[X].

But the code below produces an odd result. Yields the given traceback. My guess is that extraction succeeded but then something else failed. Evidence is that the same traceback happens whether you use the B[MyInt] version of the code or the AA version. (Previously, the AA version would work.)

object CheckOpaqueParam {
  case class Box[X](x:X)
  type B[X] = Box[X]
  @extern type MyInt = Int
  @extern type AA = Box[MyInt]
  case class A(x:B[MyInt] /*AA*/)
  def m(x: B[MyInt] /*AA*/): MyInt = A(x).x.x
}

Traceback:

[info] Compiling 31 Scala sources to /Users/savija/IdeaProjects/cake/stainless_test/verified/target/scala-2.12/classes ...
[warn] The Z3 native interface is not available. Falling back onto smt-z3.
[info] Generating VCs for those functions: 
[info] Checking Verification Conditions...
[error] Run has failed with error: java.lang.ClassCastException: class inox.ast.Types$ADTType cannot be cast to class stainless.extraction.oo.Trees$ClassType (inox.ast.Types$ADTType and stainless.extraction.oo.Trees$ClassType are in unnamed module of loader scala.reflect.internal.util.ScalaClassLoader$URLClassLoader @4b992201)
[error]