When I tried the following example, I got the error "ADT Value must appear only in strictly positive positions of Value." I got the same result using Map[String, Value].
import stainless.lang.Map
abstract class Value
case class Test(env: Map[String, Value]) extends Value
https://github.com/epfl-lara/stainless/issues/783 provides some information, although I have difficulty understanding it due to my lack of related knowledge. What I can understand is that situations like the following may cause problems:
case class Test2[K](a: K => String)
abstract class Value
case class Test(env: Test2[Value]) extends Value
When I tried the following example, I got the error "ADT Value must appear only in strictly positive positions of Value." I got the same result using Map[String, Value].
https://github.com/epfl-lara/stainless/issues/783 provides some information, although I have difficulty understanding it due to my lack of related knowledge. What I can understand is that situations like the following may cause problems:
But why is Map also being rejected? Clearly, its constructor does not include such a definition. In https://github.com/epfl-lara/stainless/blob/a38d80a8e85d085bb2e778fc8dc7668808cd6589/core/src/main/scala/stainless/verification/TypeChecker.scala#L168, we can see that the polarities of types like Map, Set, and Bag are all set to Nothing, which leads to the error message. Is this an overly conservative approach?