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.