Traceback: false missing dependency (on type parameter)

[saraswat]

Please see #773 for more background.

The code:

import stainless.annotation._
import stainless.lang.Option
object verified {
 @extern
 type B[S <: Array[S]] = Option[S]
 def m[T <: Array[T]](x: B[T]) = true
}

gives the following (surprising, "new") traceback:

[info] Compiling 31 Scala sources to /Users/savija/tmp/test/verified/target/scala-2.12/classes ...
[error] m$0 depends on missing dependencies: T$0.
[error] Cannot recover from missing dependencies
[error] ## Exception when compiling 31 sources to /Users/savija/tmp/test/verified/target/scala-2.12/classes
[error] inox.package$FatalError: Cannot recover from missing dependencies
[error] inox.Reporter.onFatal(Reporter.scala:39)
[error] inox.Reporter.fatalError(Reporter.scala:50)
[error] inox.Reporter.fatalError(Reporter.scala:98)
[error] stainless.frontend.Recovery$.recover(Recovery.scala:110)
[error] stainless.frontend.SplitCallBack.processFunction(SplitCallBack.scala:149)
[error] stainless.frontend.SplitCallBack.$anonfun$processSymbols$3(SplitCallBack.scala:138)
[error] stainless.frontend.SplitCallBack.$anonfun$processSymbols$3$adapted(SplitCallBack.scala:137)
[error] scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[error] scala.collection.Iterator.foreach(Iterator.scala:941)
[error] scala.collection.Iterator.foreach$(Iterator.scala:941)
[error] scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[error] scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[error] scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[error] stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:137)
[error] stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:67)

[saraswat]

Note that the code without type bounds works correctly:

import stainless.annotation._
import stainless.lang.Option
object verified {
@extern
 type B[S] = Option[S]
 def m[T](x: B[T]) = true
}