Skip to content

Make projections of BI operational type classes `Typeclasses Opaque`.

Robbert Krebbers requested to merge robbert/bi_tc_opaque into master

This avoids weird unification, for example where in @bupd PROP ?bupd_instance P the evar bupd_instance is unified with persistently or plainly. This occurred in practice in !843 (comment 87286), see also the test in this MR.

Note that embed was already TC opaque, but bupd/fupd/plainly/internal_eq were not.

Edited by Robbert Krebbers

Merge request reports