Failure to find a proof of persistence
Version of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
authR (prodUR (prodUR (optionUR (exclR unitO)) (optionUR (exclR unitO))) (optionUR (agreeR (boolO))))
Persistent (own γ (◯((None, None), Some (to_agree true))))
Proof search failed without reaching its limit.
if performed with
typeclasses eauto 10. It similarly doesn't work with
The statement is actually persistent, as shown by Jonas Kastberg:
Proof. apply own_core_persistent. apply auth_frag_core_id. apply pair_core_id; typeclasses eauto. Qed.
Minimal (non-)working example: https://pastebin.com/T7zhm9Zu