Improper InSet() notation when InClass() needed

[wdcraft01]

trafficstars

When providing or specifying kwarg information for domain in various expressions, we eventually check whether the specified domain is a set or a class and modify the constructed output expression accordingly, but we can still create explicit InSet() expressions involving domains that are actual classes. It could be important to avoid this possibility, and recently @wwitzel suggested we raise a ValueError when the system attempt to construct an InSet expression involving a domain that is a class instead of a set.

Some brief related background. For example, in a Forall expression like this:

Forall(x, P(x), conditions = [LessEq(x, 0)], domain = Integer),

the constructed expression uses the InSet notation to produce the equivalent of:

$\forall_{x \in \mathbb{Z} | x \le 0}\big[P(x)\big]$

because the system knows that Integers is a legitimate set (and not a class). On the other hand, for the Forall expression:

Forall(V, P(V), domain = VectorSpacs(Real)),

the constructed expression automatically uses the InClass notation to produce the equivalent of:

$\forall_{V \underset{{\scriptscriptstyle c}}{\in} \mathrm{VecSpaces}}\big[P(V)\big]$

because the system knows that the collection of vector spaces over the field of Reals is actually a proper class.

For the Forall and other OperationOverInstances expression, the InSet vs. InClass distinction is caught at the level of the OperationOverInstances, where the construction of the OperationOverInstances checks to see if the domain has an is_proper_class attribute that is True. Interestingly, even when a possible domain is actually a class instead of a set, the user can still explicitly form InSet expressions using the domain. So, for example, there is nothing to keep a user from constructing the expression:

$V \in \textrm{VecSpaces}$

and then using that membership claim in other expressions. This allows the user, for example, to do something like this:

Forall(V, Function(P, V), conditions = [InSet(V, VecSpaces(Real))]),

short-circuiting the automatic InClass notation associated with the domain and producing the expression:

$\forall_{V \in \mathrm{VecSpaces}}\big[P(V)\big]$.