Hint Immediate plain_persistent affects type inference of unrelated variables
I reproduced the same issue as stdpp!424 (closed) / stdpp#160 (closed). Below, notice how evar ?T
is instantiated with Plain P
, and how that stops once we replace the `Hint Immediate.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Section foo.
Context (PROP : bi) `{BiPlainly PROP}.
Implicit Type (P : PROP).
Lemma test P `{!Affine P} `{!Plain P} :
∃ T : Type, T -> P ⊢ □ P.
Proof.
eexists.
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
============================
?T → P -∗ □ P
*)
iIntros (X) "#?".
Show.
(*
1 goal
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
X : Plain P
============================
_ : P
--------------------------------------□
□ P
*)
Abort.
Local Remove Hints plain_persistent : typeclass_instances.
(* An instance would be enough locally: *)
(* Local Existing Instance plain_persistent. *)
(* but we sketch the proper fix. *)
Ltac solve_tc_onestep :=
solve [once (typeclasses eauto 1)].
Local Hint Extern 1 (Persistent _) =>
notypeclasses refine (plain_persistent _ _); solve_tc_onestep : typeclass_instances.
Lemma test P `{!Affine P} `{!Plain P} :
∃ T : Type, T -> P ⊢ □ P.
Proof.
eexists.
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
============================
?T → P -∗ □ P
*)
iIntros (X) "#?".
Show.
(*
1 focused goal (shelved: 1)
PROP : bi
H : BiPlainly PROP
P : PROP
Affine0 : Affine P
Plain0 : Plain P
X : ?T
============================
_ : P
--------------------------------------□
□ P
*)
Edited by Paolo G. Giarrusso