Function value can depend on set of allocated objects (part of #1419)

[cpitclaudel]

I'm creating a new issue to track the more complex parts of #1419 that popped up in the discussion of #1924 and led to #1936.

Reference case: for datatypes, we need to check recursively, not just the type parameters:

class C {}
datatype D = DC(c: C)
type X(!new) = D // No error

datatype Obs' = Obs'(s: set<object>)
predicate lotsOfObjects'() {
  exists o: Obs' :: |o.s| > 10 // No error
}

Another example:

class C {}

datatype Box<T> = Box(t: T)
type Box'(!new) = Box<C> // Rejected

datatype BoxC = BoxC(c: C)
type BoxC'(!new) = BoxC // No error

[cpitclaudel]

Closed in #1924