could not find instance of pattern

Stream: general

[Bhakti Shah]

I'm getting a really weird error that I suspect has to do with typeclass derivations but I might be entirely wrong. I'm trying to rewrite using this theorem:

inSet : [BEq α], α -> Set α -> Bool
InSet : α -> Set α -> Prop
theorem inSetPropBoolEquiv [DecidableEq α] {a : α} {as : Set α} : inSet a as = true <-> InSet a as

which is kind of an analogue of these list lemmas.

my goal state has this:

f : A
pset : Set A
---
inSet f pset = true

but when i try to rw [inSetPropBoolEquiv], I get this error:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  inSet ?m.113395 ?m.113396 = true

which doesn't make sense to me because that is the form my goal is in. I thought it might be a DecidableEq instance thing but A is an instance of DecidableEq so that doesn't make sense. Am I missing something obvious?

[Bhakti Shah]

[Edit: deleted because it was wrong and irrelevant to the original question]

[Kevin Buzzard]

That's a type error. The error says that you're not putting your inputs in the correct places.

[Bhakti Shah]

Ah i see. fully qualified it correctly

rw [@inSetPropBoolEquiv A instDecidableEqA f pset]

and I got the same error as before of the rewrite failure, which I'm still unable to solve.

[Bhakti Shah]

I solved it. So for A I had deriving BEq, DecidableEq for A (at some point I had only BEq and added DecidableEq later, but now I realize that you don't need both), and it generated two separate instBEq instantiations -- one directly via the BEq and one via the DecidableEq. inSet's BEq constraint was then filled by two different instances in the target and the pattern and hence could not be unified, and since it was an implicit arg it was never printed; I just happened to notice it when I hovered over the term in the goal panel :')

[Bhakti Shah]

Maybe an opportunity to improve the error message on unification failure? explicitly mentioning which argument could not be unified would be useful