Inline trivial lambda bindings, to beta-reduce later on for smaller scripts

[kk-hainq]

A long-overdue continuation of #4219.

The back-story is that we wanted to have a flag that removes traces for slightly smaller scripts without changing the source code. However, #4219 only ignores the trace text and more or less keeps the trace bindings intact, only removing trace messages and reducing little CPU usage at run time.

To inline and later beta-reduce the new definition for actual smaller scripts, we would need a very specific case in trivialTerm:
https://github.com/input-output-hk/plutus/blob/c8c5183f7facd967d48fe07b3b14465b8dd48fe7/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs#L312-L325

TyAbs _ _ _ (LamAbs _ _ _ (LamAbs _ n _ (Var _ n'))) | n ^. theUnique == n' ^. theUnique -> True

This can be generalized as followed like in this PR:

TyAbs _ _ _ t  -> trivialTerm t
LamAbs _ _ _ t -> trivialTerm t

Meaning we would like to inline (to later beta reduce) trivial lambda bindings. This looks pretty scary at a glance without any depth check or concrete definition of triviality, but early experiments suggest that there are not many such bindings in practice:
IntersectMBO/plutus-apps#219.

I guess this is more of an issue with code samples than an actual PR. Would love to receive some inputs before continuing it. Another adventurous line is to try inlining bindings that are applications, like in:
https://github.com/input-output-hk/plutus/blob/c8c5183f7facd967d48fe07b3b14465b8dd48fe7/plutus-tx-plugin/test/Plugin/NoTrace/Spec.hs#L48-L51

Pre-submit checklist:

• Branch
  • Tests are provided (if possible)
  • Commit sequence broadly makes sense
  • Key commits have useful messages
  • Relevant tickets are mentioned in commit messages
  • Formatting, materialized Nix files, PNG optimization, etc. are updated
• PR
  • (For external contributions) Corresponding issue exists and is linked in the description
  • Self-reviewed the diff
  • Useful pull request description
  • Reviewer requested

[michaelpj]

This needs a note. The decision making here is actually quite complicated. We need to think about two things: saving work, and saving space.

In terms of saving work, I think this is fine. We will create the outermost lambda value at each use site instead of once, but that's a pretty small amount of work that I'm fairly okay with rounding to 0 (but we should document that in a note!). Indeed, several of the other cases also require us to do value creation at each use site, although creating lambda values is probably the most expensive kind (not by much).

In terms of saving space, this is riskier. We will duplicate the whole term at each use site. The other cases all relate to terms which are approximately the same size as a variable (except the constant case! which has a worrying TODO on it...). We could make this much safer by actually doing something more like what the GHC inliner does, and conditionally inlining things at call sites if they're fully applied. But this would be much more complicated...

I think for starters this could do with:

• A note
• Splitting up this function into two that represent the two decisions that we're making. Something like costIsAcceptable and sizeIsAcceptable. That way it's clearer what they're checking for and we could in principle use them separately if that's appropriate elsewhere. Then postInlineUnconditional can require that both hold.

Suggested implementations:

costIsAcceptable = \case
  Builtin{} -> True
  Var{} -> True
  Constant{} -> True
  LamAbs{} -> True
  TyAbs{} -> True
  Error{} -> True
  IWrap _ _ _ t -> costIsAcceptable t
  Unwrap _ t -> costIsAcceptable t

  Apply{} -> False
  TyInst{} -> False
  Let{} -> False

sizeIsAcceptable = \case
  Builtin{} -> True
  Var{} -> True
  -- These are the two dubious cases, note here
  LamAbs _ _ _ t -> sizeIsAcceptable t
  TyAbs _ _ _ t -> sizeIsAcceptable t
  Error{} -> True
  
  Constant{} -> False --- I actually think inlining constants is pretty dubious 
  -- Arguably we could allow these two...
  IWrap _ _ _ t -> False
  Unwrap _ t -> False
  Apply{} -> False
  TyInst{} -> False
  Let{} -> False

[michaelpj]

This is a bit subtle, and we need to be careful about the reasoning. If you've got time to think more about this I have some suggestions, otherwise I might just push some tweaks to this branch.

[michaelpj]

I'm going to write a patch, sorry. I need to write a bit about the tradeoffs, better for me to do it!

[kk-hainq]

@michaelpj Yeah, I did run out of my depth there. I only felt scared inlining deep lambdas and that was it... I guess I can test your upcoming patch in different places to see if anything strange happens.

[michaelpj]

Done and merged separately.