Skip to content

Demand: Don't rewrite `CS(S)` to `S` (#21085)

Sebastian Graf requested to merge wip/T21085 into master

In #21085 (closed) we established that we have CS(S) > S, otherwise plusSubDmd is non-monotone:

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

That means that CS(S) /= S and we may not do the rewrite from CS(S) to S in mkCall. We may still rewrite S to CS(S) in viewCall, which is a monotone transition, in that

viewCall S = CS(S) <= CS(S) = viewCall CS(S)

We still have L=CL(L), so we are allowed to rewrite it in mkCall.

See also the new Note [Do not rewrite CS(S) to S].

Fixes #21085 (closed).

Merge request reports