Closures probably not that less efficient

[workingjubilee]

In Section 5.5 of https://arxiv.org/pdf/2108.02995.pdf it is asserted:

Partial applications.

Rust requires all functions to be fully applied when called, unlike Coq which supports partial application. Partial applications can be emulated easily through closures, by generating both curried versions and uncurried versions of functions. However, using closures is less efficient, so as an optimization the extraction avoids closures when possible. Concretely, this results in both curried and uncurried versions as is seen in the extraction above, with the curried version calling into the uncurried version.

This is somewhat unwarrantedly imprecise as in many cases, the actually-optimized code will yield as-good or even better performance than its unclosured form, as discussed in chapter 13, section 4 of TRPL. The code in question may actually optimize better if it doesn't first have to inline the uncurried version. If information was obtained to prove either way, that would be interesting to know. That said, all the monomorphization concerns you said apply, so this may be irrelevant as an issue.

[workingjubilee]

Forcing vtables is probably also bad for code size (optimizing them away is harder than optimizing other things away), and should be avoided if it is unnecessary.