Prevent iFrame from unfolding definitions?
Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding tc_opaque
, but many people don't know to do that and experience large iFrame
slowdowns when piling up abstractions.
It'd be good to investigate whether we can somehow make definition-unfolding for iFrame
be opt-in rather than opt-out.
One possibility is to use Hint Extern
, like SetUnfold
. However, that does not allow users to opt-in.
Another possibility would be to use a different hint database where constants are by default opaque.
Either way this is a massive breaking change and would have to be carefully evaluated.