Demand: `plusSubDmd` does not preserve `Eq SubDemand`

It appears that plusSubDmd is not well-defined wrt. Eq SubDemand. Consider

L + S = S = CS(S) < CS(L) = C(L+S)(LuS) = L + CS(S)

(Recall that L=[0,ω], S=[1,ω].)

That is, although S == CS(S), we have L+S /= L+CS(S).

I'm unsure what the practical consequences are. The same holds if you replace S with B, by the way, but we don't allow CB(B) as a demand at the moment (because B is not a CardNonAbs).

This could probably be fixed by saying S < CS(S) instead of equating both. I think our definition of lubSubDmd (which I wrote u above) already does that. In practice, the only change would be not to rewrite non-L call sub-demands Cn(n) to their polymorphic counterpart n in mkCall. So no turning CS(S) into S. CA(A) and CB(B) can't be build anyway (because they aren't CardNonAbs), although they can still occur through viewCall. I don't think that's harmful, as viewCall (the rewrite S to CS(S), as opposed to the other direction) is monotone.

---

Also note that this happens because plusSubDmd and lubSubDmd differ for the relevant cardinalities involved, and we define C^n1(d1) + C^n2(d2) = C^(n1+n2)(d1 u d2). Thus it is in theory not unique to strictness demands. Here's a similar example for upper bound 1 (where 1+1=ω/=1=1u1):

1 + 1 = S = CS(S) > CS(1) = C(1+1)(1u1) = C1(1) + C1(1)

Note that the direction of the inequality is the other way around here, which implies we may not expand 1 to C1(1) (because that improves precision), but contract C1(1) to 1 (which loses information).

Ah, but appears that we ban at-most-once cardinalities in Poly already (Note the CardNonOnce), so this latter example isn't a problem in practice.