From 4cfa2e8a591fb5cfc6aa6e7d1ba60b771f1d74f1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 19 Sep 2017 19:48:11 +0200 Subject: [PATCH] Remove workaround. This bug is strange: - In order to type check the argument `I : gmap lft lft_names`, Coq needs an instance `Countable lft`. Since `finite.finite_countable` has been declared using `Hint Immediate` it will try that instance first (*), which means it has to find an instance `Finite lft`. - Apparently, at this moment the type of the argument `A` has not been inferred by the type checker yet. So, there is a hypothesis `A : ?T`. - In order to prove `Finite lft`, Coq unifies `?T` with `Finite lft` and uses the hypothesis `A`. - Subsequent type checking fails, because `gmap lft lft_names` is type checked using a wrong/arbitrary instance `Countable lft`. This is probably a Coq bug: type class search should not just unify with hypotheses whose type is just an evar. (*) `finite.finite_countable` has been declared using `Hint Immediate` to make sure it is only used at leafs, not to make sure that it is used first. --- theories/lifetime/model/creation.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v index b25469ef..c0caed9a 100644 --- a/theories/lifetime/model/creation.v +++ b/theories/lifetime/model/creation.v @@ -55,11 +55,7 @@ Proof. iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame. Qed. -(* FIXME: Get rid of this hack. If we just remove this line, the next lemma - statement breaks. *) -Remove Hints finite.finite_countable : typeclass_instances. - -Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) : +Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lft) : let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in K ⊥ K' → (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) → -- GitLab