frame_instances: revise priorities for uses in "linear" bi
Note: For the purposes of this MR, "linear bi" includes those where
BiAffine instances aren't available to proof search.
- I pre-discussed this with @robbertkrebbers in https://mattermost.mpi-sws.org/iris/pl/wks7ckrj4j8g9docyjq7s3iy5y, but here's a self-contained summary:
The new workings are documented in the code. Today, instead,
frame_here_absorbing | 0 will seldom succeed, so
frame_here | 1, but after other hints like
frame_exist | 1. So, to frame
R is an existential,
iFrame will first try to pull the existential apart before framing
R as a whole, which might be expensive (especially for overly large
Rs). The same applies to other connectives.
- For each instance, I added either an explicit priority or a comment, but I'm sure you might have different preferences.
Please count this as a Bedrock contribution — we've hit this in practice (and we've also sealed the offending