ADT must appear only in strictly positive positions when using Map

[LioTree]

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

#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

But why is Map also being rejected? Clearly, its constructor does not include such a definition. In

stainless/core/src/main/scala/stainless/verification/TypeChecker.scala

Line 168 in a38d80a

def polarity(polarities: mutable.Map[(Identifier,Identifier),Polarity]) = Nothing

, 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?