Drop redundant unsafeCaseList calls produced by AsData

[zliu41]

This makes AsData generate much more optimal code. See Note [Dropping redundant unsafeCaseList calls produced by AsData].

[github-actions]

Execution Budget Golden Diff

2fad725 (master) vs 82933e7

output

plutus-benchmark/cardano-loans/test/9.6/main.golden.eval

Metric	Old	New	Δ%
Flat Size	8_698	8_695	-0.03%

plutus-tx-plugin/test/AsData/Budget/9.12/richSumSingleField.golden.eval

Metric	Old	New	Δ%
CPU	717_432	461_432	-35.68%
Memory	4_364	2_764	-36.66%
Flat Size	105	66	-37.14%

plutus-tx-plugin/test/AsData/Budget/9.6/richSumSingleField.golden.eval

Metric	Old	New	Δ%
CPU	717_432	461_432	-35.68%
Memory	4_364	2_764	-36.66%
Flat Size	105	66	-37.14%

This comment will get updated when changes are made.

[zliu41]

Regarding the changes in the constitution scripts, see #7681

[SeungheonOh]

The optimizations are very good; I don't particularly like having extra optimization pass and annotation for dropping cases since they introduces extra complexity on the annotation interface and they are very specific to Data matching in particular.

Being said, I don't think there's an easy way to do this on TH so this is probably best approach with minimal change. And all the changes looks good with some minor suggestions.

[SeungheonOh]

Is there any reason we only check two nested lambdas? I think it should work on arbitrarily nested lambdas. So

When we have
case scrut [\a b ... y z -> <handler>]

this case should be dropped if case is marked safe to drop and <handler> doesn't use a b ... y z.

[zliu41]

I'm only thinking about casing on lists. But I agree we can make it more general.

[zliu41]

It's actually not easy to generalize this. In general, it's incorrect to simply drop all binders. To determine how many binders to drop, you'd need to run the type checker. Which is doable, but will make this pass a lot more complicated. I'd prefer keeping things simple for now, and going that route when it becomes necessary.

[SeungheonOh]

But don't we have same problem on the two nested-lambda case as well? For example, if we mark below Case safe to drop, it will break the types

[(case (constr 0) [\a b x y -> x + y]) 1 2 3 4]

as we will optimize this into

[(\x y -> x + y) 1 2 3 4]

which is incorrect.

But I think it's okay to keep as is since it's mainly just for optimizing casing on list. We can make this optimization more general once we have other places to run this optimization on.

[zliu41]

But I think it's okay to keep as is since it's mainly just for optimizing casing on list. We can make this optimization more general once we have other places to run this optimization on.

Exactly.

[Unisay]

richSumSingleField goldens look good (−36% CPU, −52% AST).

[Unisay]

JFYI: I tried this to handle any number of LamAbs binders, not just two:

processTerm = \case
  Case a _resTy _scrut [branch]
    | annIsSafeToDrop a
    , let (binders, body) = peelLamAbs branch
    , not (null binders)
    , let usages = Usages.termUsages body
    , all (\b -> Usages.getUsageCount b usages == 0) binders ->
        body
  other -> other

peelLamAbs :: Term tyname name uni fun a -> ([name], Term tyname name uni fun a)
peelLamAbs (LamAbs _ n _ inner) = let (ns, body) = peelLamAbs inner in (n : ns, body)
peelLamAbs t = ([], t)

[zliu41]

This is incorrect, because the type of body may not match _resTy (e.g., consider case list [f]). They must match.