`solve_proper` on fails/succeeds depending on presence of coercion
On Mattermost @vsiles and I had a discussion about the coercion sem_ty_car
in the POPL'20 tutorial. We believe it should be removed because it causes more confusion than it does good.
I tried to remove the coercion but came to the unpleasant surprise that it causes solve_proper
to fail. This is strange, since the behavior of solve_proper
depends on the presence of a coercion, which IMHO makes no sense.
Below I have included a minimized example.
From iris.heap_lang Require Import derived_laws.
Record sem_ty Σ := SemTy { sem_ty_car : val → iProp Σ }.
Arguments SemTy {_} _%I.
Arguments sem_ty_car {_} _ _ : simpl never.
Section sem_ty_cofe.
Context {Σ : gFunctors}.
Instance sem_ty_equiv : Equiv (sem_ty Σ) := λ A B,
∀ w, sem_ty_car A w ≡ sem_ty_car B w.
Instance sem_ty_dist : Dist (sem_ty Σ) := λ n A B,
∀ w, sem_ty_car A w ≡{n}≡ sem_ty_car B w.
Lemma sem_ty_ofe_mixin : OfeMixin (sem_ty Σ).
Proof. by apply (iso_ofe_mixin (sem_ty_car : _ → val -d> _)). Qed.
Canonical Structure sem_tyO := Ofe (sem_ty Σ) sem_ty_ofe_mixin.
Global Instance sem_ty_car_ne n : Proper (dist n ==> (=) ==> dist n) sem_ty_car.
Proof. by intros A A' ? w ? <-. Qed.
End sem_ty_cofe.
Definition sem_ty_prod {Σ} (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ sem_ty_car A1 w1 ∧ sem_ty_car A2 w2)%I.
Global Instance sem_ty_prod_ne Σ : NonExpansive2 (@sem_ty_prod Σ).
Proof.
Fail solve_proper.
Abort.
(** Now let's add a coercion, this somehow makes sure that [solve_proper] works *)
Coercion sem_ty_car : sem_ty >-> Funclass.
Global Instance sem_ty_prod_ne Σ : NonExpansive2 (@sem_ty_prod Σ).
Proof. solve_proper. Qed. (* works *)
Edited by Robbert Krebbers