Provide some way to "seal" a BI
One reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms in general are just bigger.
It might be worth investigating some nice way to seal a BI (but that would probably have to be a macro):
- either lightweight sealing by just making it TC opaque and forwarding all instances
- or a proper seal that makes terms no convertible any more, and a lot of forwarding of things
We do seal iProp
pretty heavily (in fact even more proper than the "proper" seal, this is the one place where we use a module type for sealing to be really sure), so Iris itself doesn't have this problem.
@robbertkrebbers IIRC you did an experiment along the lines of doing that by hand once? What were the results of that again?