Refactor Demand lattice so that it has less semantic equalities
Since !4371 (closed), Demand
is defined pretty simply as data Demand = Card :* SubDemand
. But for absent demands (e.g. when Card
is C_00
or C_10
), the SubDemand
doesn't actually make sense because it describes how the thing is evaluated nestedly, if it is evaluated at all. If the premise is never satisfied, as for absent demands, that information is never useful. We should make use sites aware of that fact, so they pick whatever SubDemand
they want for absent demands.
More concretely, this ticket is about assessing whether we can bring back some of the demand structure we had before !4371 (closed) and refactor to:
data Card = C_01 | C_0N | C_11 | C_1N -- NB: C_00 and C_10 are gone!
data Demand = Absent | Bottom | Card :* SubDemand
data SubDemand = Poly Card | Prod [Demand] | Call Demand
Note that Call
now takes a Demand
instead of a Card
and a SubDemand
separately. The interpretation of that demand is a little different than those demands inside a product, particularly around plusSubDmd
, because call demands are relative, whereas product demands are ... at least in part absolute (cf. #18885 (closed)). Nevertheless, the analogy is fitting: The demand Edit: No, really it is not: 1C(A)
then says "evaluated once and called with one argument, but not called further".1C(A)
means "evaluated once but never called", because the Card
of the Demand
expresses how often the thing is called. Better use Poly C_00
here. UC(1C(1U)
means "evaluted multiple times, but called exactly one with two arguments" and so on.
Let's see whether that works.