Typeclass interference does not work for Timeless (□ P)
In the following code I would expect the first apply _
to work. Instead affinely_timeless
has to be applied explicitly before apply _
works.
Instance timeless (P : iProp Σ) `{!Timeless P} : Timeless (□ (P)).
Proof.
Fail apply _.
eapply affinely_timeless; by apply _. (* this goes through *)
Qed.