Skip to content

`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

Robbert Krebbers requested to merge robbert/pm_unify_class into master

This has the following advantages:

  • We need fewer adhoc Hint Extern instances for the proof mode, we can just use Unify.
  • We can consistently use the refine unification algorithm when trying to unify a hypothesis/conclusion of a lemma/wand to the goal. This is currently only done by iAssumption, but not by iFrame or iApply.
  • It might allow us to use Typeclasses Opaque for all std++ operational type classes. As described in !914 (comment 91480), this is currently impossible.

We could probably do some bikeshedding about the name or other implementation aspects. But I might make sense to first check out the performance impact and whether it breaks anything in the reverse dependencies. So @jung could you run timing CI, please.

Edited by Ralf Jung

Merge request reports