Infer needed `zero_alloc` checks from signatures

[ccasin]

In the "zero_alloc in signatures" work, we made it so that to expose a function as zero alloc in your signature, you must also put a zero_alloc attribute on it in the structure. This guarantees the backend check will run on that function, as implied by the signature. But also it's a real pain to write the attribute in two places, and we can do better: This PR lets the user skip writing the attribute on the implementation and infers that the check is needed from the signature.

There are three commits, the first two of which are refactoring. I suggest the main reviewer reads commit by commit. 1) The first commit makes a change that was suggested for the original signatures work. It changes the way we store zero_alloc attributes on applications to be the syntactic version of those attributes rather than their values in the semantic domain. At the same time, it changes when we check whether we can infer [@zero_alloc assume] on an application - now we do this during translation to lambda rather than when typechecking the application. This is helpful in later commits - we are delaying that inference step until it is safe to default zero_alloc variables. 2) The second commit moves the logic for checking whether one zero_alloc attribute is at least as strong as another out of Include_core and into its own file. It makes sense to have this together with the implementation of zero_alloc variables (which comes in the next commit), and I've made it its own commit so that I'm not both moving and changing that code in one commit. 3) The third commit implements inference and adds tests. If a function definition has no zero_alloc attribute on it we make a variable representing whether or not it will need to be checked. That variable can be filled in when we compare the module to its signature. These variables are somewhat simpler than jkind or type variables because we never need to link two of them.

I suggest @ncik-roberts reviews, as he did for the signatures implementation. @gretay-js should take a look at the tests, at least.

This PR does not yet make it so that zero_alloc information is carried across aliases (let f = g) - there is enough here that I think that should be its own PR.

One minor design note:

Locations in errors

Today zero_alloc errors look like this:

File "/home/ccasinghino/tmp/foo.ml", line 1, characters 5-15:
1 | let[@zero_alloc] f x = (x,x)
         ^^^^^^^^^^
Error: Annotation check for zero_alloc failed on function Foo.f (camlFoo__f_0_1_code)

File "/home/ccasinghino/tmp/foo.ml", line 1, characters 23-28:
1 | let[@zero_alloc] f x = (x,x)
                           ^^^^^
Error: allocation of 24 bytes

The error has two parts: The first identifies the location of the attribute that said to check something. The second shows the offending allocation.

After this PR, the attribute that caused the check may be far removed from the implementation, off in a signature somewhere. Making that show up first in the error seems bad for editor integration - people probably want to navigate to the offending function. So if the check is an inferred one, I've made the first error point to the function that was checked instead.

I'm not sure that's exactly the right place to point. Also it would probably be convenient to know what attribute caused this check, somehow, even if that's not going to be the place we most commonly want to navigate. That information is easy to make available, but I think the right thing is to pass it to the backend and have the backend include it later in the error, and propose putting that off for a future PR.

[ccasin]

I've reworked this slightly to offer nicer inference behavior, and rebased/squashed to give it a nice history. Nothing about the original PR description needs changing.

One interesting note, pointed out by Leo, is that the rules for zero_alloc variables are similar to the rules for modalities on the comonadic (prescriptive) axes. In typemod I've slightly generalized the infrastructure to support those that was just added in #2685 and renamed the functions to, hopefully, explain their purpose more clearly, make clear that they are doing something similar to remove_mode_and_kind_variables, and be clear they deal with both modalities and zero_alloc variables.

[ccasin]

Thanks for the review. I think I've addressed all the minor stuff and will play around with the types in typedtree sometime in the next few days.

[ccasin]

Thanks for the changes. I think the type refactoring you did in the latest commit is nice and helps make some non-obvious (or comment-enforced) invariants much clearer. I haven't checked whether additional type refactors would be nice in the same way, but you can make the call.

Thanks. I did look for additional opportunities to make this kind of change, but didn't find them, because the other places where zero_alloc stuff appears in types or the typedtree need the option to be variables.