I had to think about this for a bit but yeah, this should work. Can we get a variant of #5672 that tests this case. Obviously we have a bug at the moment, but in future hopefully not.

I wanted to add a test case for let addInteger = \x y -> (builtin addInteger) x y, but it needs on the problem shown in #5672 to be fixed, so let me do that first.

I'm somewhat tempted to say that that's a limitation of the inliner that we should try to fix. I'm not sure how big a deal it is if this doesn't work as effectively for effectful args, but only running the inliner once seems attractive.

I'd like to see how much a difference it makes if we just do it once.

Okay, I tried it and things are much worse. However, I think this is not so much to do with effectful terms. It's to do with type arguments. We have long had the problem that you can't beta-reduce all the arguments at once for a term with type and term arguments. You end up with something like this:

map = (/\ a b . \(f :: a -> b) (l :: List a) . ...) {integer} {integer} incInteger ls
--->
(let
  a = integer
  b = integer
in \(f :: a -> b) (l :: List a) . ...)) incInteger ls

Whereas if we produced this:

let
  a = integer
  b = integer
  f :: a -> b = incInteger
  l :: List a = ls
in ...

the bindings for f and l don't typecheck, because their signatures reference the type variables, but their RHSs need the type variables to have been substituted in.

So we end up awkwardly having to do one beta, inline the type variable (which we don't always do!) and then do the rest of the arguments. This plausibly blocks a bunch of optimzation, with this being one example.

It would be good to improve this. It's not as simple as just always inlining type variables, because this is exactly the situation that we have when we compile down datatypes, and we really don't want to inline all of those otherwise we get truly enormous programs and the typechecker grinds to a halt.

However, I think it would be safe to always inline type variables just when doing call-site inlining, because we have the size check, so that won't let us actually grow the program!

I think this is not so much to do with effectful terms

It does have to do with effectful terms in the let addInteger = \x y -> (builtin addInteger) x y case (because running it once is not enough in this case), but maybe that isn't the main reason that it got much worse.

However, I think it would be safe to always inline type variables just when doing call-site inlining, because we have the size check, so that won't let us actually grow the program!

This sounds questionable: the size check arguably should not include the types in the first place, because ultimately we care about the UPLC size, not the PIR size.

It does have to do with effectful terms in the let addInteger = \x y -> (builtin addInteger) x y case

Why are the arguments effectful there?

This sounds questionable: the size check arguably should not include the types in the first place, because ultimately we care about the UPLC size, not the PIR size.

This is not true: if we let the size of the types get out of control we will slow down the typechecker and compiler to the point of unusablity. I know this because it happened once when we accidentally inlined all type variables. I agree it's a wart.

I'm not convinced that this isn't also exponential... why do we think that?

I notice that what we actually want to do is even simpler than running unconditional inlining: we want to do unconditional inlining, only considering bindings from the current term, and then just apply the substitution if we have one. I'm not sure if it's easy to express that, but it might make this less expensive.

I thought it would be similar as what we currently do but that's not the case, and it can indeed be exponential. A term can be processed for unconditional inlining twice, so its subterms can be processed four times, eight times etc.

That said it is extremely unlikely to be a problem in practice, so I'm inclined to say that it is not worth having a "simpler unconditional inlining" implementation just for this.

inline' does still redundantly compute the term usages.

I'm not sure why we can't just call processTerm here? We're in InlineM, so we can just do that directly and not define inline' at all.

The first argument of applyAndBetaReduce is the renamed RHS. Since it has been renamed, usage account needs to be re-done.

In fact, because the RHS is renamed, we'll also need to re-calculate the VarsInfo (which I'm not doing currently), and merge it with the original VarsInfo. I'll update it.

Ouch. If we're going to do that, you could compute it locally, merge it with the ones in the context using local, and then just call processTerm. I think that would be neater IMO.

Although maybe you would still need to recompute this information for each iteration, because if inlining actually inlines stuff, now we have newly renamed variables in the term. Possibly we can just ignore those, though. Again, it would be much simpler if we were just running the inliner once.

A further observation: we only need to rename the term when we substitute it in. I think it is in fact fine to do the application-and-beta-reduction step on the non-renamed term. After all, the original term came from elsewhere in the program and we have globally unique names. We just want to make sure that if we insert a copy of it into the main program, that final copy has new names.

A further observation

Grr, this is not true because of the inliner state, which is kept in StateT, so if we ran processTerm, we'd add mappings for stuff we inline to that, and they would persist and potentially be used later where they shouldn't be. So we would need to either rename or only locally modify the state.